1 /-
2 Copyright (c) 2018 Sébastien Gouëzel. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Sébastien Gouëzel
5 Adapted from the corresponding theory for complete lattices.
6
7 Theory of conditionally complete lattices.
8
9 A conditionally complete lattice is a lattice in which every non-empty bounded subset s
10 has a least upper bound and a greatest lower bound, denoted below by Sup s and Inf s.
11 Typical examples are real, nat, int with their usual orders.
12
13 The theory is very comparable to the theory of complete lattices, except that suitable
14 boundedness and nonemptiness assumptions have to be added to most statements.
15 We introduce two predicates bdd_above and bdd_below to express this boundedness, prove
16 their basic properties, and then go on to prove most useful properties of Sup and Inf
17 in conditionally complete lattices.
18
19 To differentiate the statements between complete lattices and conditionally complete
20 lattices, we prefix Inf and Sup in the statements by c, giving cInf and cSup. For instance,
21 Inf_le is a statement in complete lattices ensuring Inf s ≤ x, while cInf_le is the same
22 statement in conditionally complete lattices with an additional assumption that s is
23 bounded below.
24 -/
25 import
26 order.lattice order.complete_lattice order.bounds
src └───────────┘ └────────────────────┘ └──────────┘
27 tactic.finish data.set.finite
src └───────────┘ └─────────────┘
28
29 set_option old_structure_cmd true
doc └───────────────┘
30
31 open set lattice
32
33 universes u v w
34 variables {α : Type u} {β : Type v} {ι : Sort w}
35
36
37 section
38
39 /-!
40 Extension of Sup and Inf from a preorder `α` to `with_top α` and `with_bot α`
41 -/
42
43 open_locale classical
44
45 noncomputable instance {α : Type*} [preorder α] [has_Sup α] : has_Sup (with_top α) :=
id └──────┘ ┴ └─────┘ ┴ └─────┘ └──────┘ ┴
src └──────┘ └─────┘ └─────┘ └──────┘
typ └──────┘ ┴ └─────┘ ┴ └─────┘ └──────┘ ┴
doc └─────┘ └─────┘
46 ⟨λ S, if ⊤ ∈ S then ⊤ else
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
47 if bdd_above (coe ⁻¹' S : set α) then ↑(Sup (coe ⁻¹' S : set α)) else ⊤⟩
id └───────┘ └─┘ └─┘ ┴ └─┘ ┴ ┴ └─┘ └─┘ └─┘ ┴ └─┘ ┴ ┴
src └───────┘ └─┘ └─┘ └─┘ ┴ └─┘ └─┘ └─┘ └─┘ ┴
typ └───────┘ └─┘ └─┘ ┴ └─┘ ┴ ┴ └─┘ └─┘ └─┘ ┴ └─┘ ┴ ┴
doc └───────┘ └─┘ └─┘ └─┘
48
49 noncomputable instance {α : Type*} [has_Inf α] : has_Inf (with_top α) :=
id └─────┘ ┴ └─────┘ └──────┘ ┴
src └─────┘ └─────┘ └──────┘
typ └─────┘ ┴ └─────┘ └──────┘ ┴
doc └─────┘ └─────┘
50 ⟨λ S, if S ⊆ {⊤} then ⊤ else ↑(Inf (coe ⁻¹' S : set α))⟩
id ┴ ┴ ┴ ┴┴ ┴ ┴ └─┘ └─┘ └─┘ ┴ └─┘ ┴
src ┴ ┴┴ ┴ ┴ └─┘ └─┘ └─┘ └─┘
typ ┴ ┴ ┴ ┴┴ ┴ ┴ └─┘ └─┘ └─┘ ┴ └─┘ ┴
doc └─┘ └─┘
51
52 noncomputable instance {α : Type*} [has_Sup α] : has_Sup (with_bot α) :=
id └─────┘ ┴ └─────┘ └──────┘ ┴
src └─────┘ └─────┘ └──────┘
typ └─────┘ ┴ └─────┘ └──────┘ ┴
doc └─────┘ └─────┘
53 ⟨(@with_top.lattice.has_Inf (order_dual α) _).Inf⟩
id └──────────────────────┘ └────────┘ ┴ └─┘
src └──────────────────────┘ └────────┘ └─┘
typ └──────────────────────┘ └────────┘ ┴ └─┘
doc └────────┘
54
55 noncomputable instance {α : Type*} [preorder α] [has_Inf α] : has_Inf (with_bot α) :=
id └──────┘ ┴ └─────┘ ┴ └─────┘ └──────┘ ┴
src └──────┘ └─────┘ └─────┘ └──────┘
typ └──────┘ ┴ └─────┘ ┴ └─────┘ └──────┘ ┴
doc └─────┘ └─────┘
56 ⟨(@with_top.lattice.has_Sup (order_dual α) _ _).Sup⟩
id └──────────────────────┘ └────────┘ ┴ └─┘
src └──────────────────────┘ └────────┘ └─┘
typ └──────────────────────┘ └────────┘ ┴ └─┘
doc └────────┘
57
58 end -- section
59
60 namespace lattice
61 section prio
62 set_option default_priority 100 -- see Note [default priority]
doc └──────────────┘
63 /-- A conditionally complete lattice is a lattice in which
64 every nonempty subset which is bounded above has a supremum, and
65 every nonempty subset which is bounded below has an infimum.
66 Typical examples are real numbers or natural numbers.
67
68 To differentiate the statements from the corresponding statements in (unconditional)
69 complete lattices, we prefix Inf and Sup by a c everywhere. The same statements should
70 hold in both worlds, sometimes with additional assumptions of nonemptiness or
71 boundedness.-/
72 class conditionally_complete_lattice (α : Type u) extends lattice α, has_Sup α, has_Inf α :=
id └──┘ └─────┘ ┴ └─────┘ ┴ └─────┘ ┴
src └─────┘ └─────┘ └─────┘
typ └──┘ └─────┘ ┴ └─────┘ ┴ └─────┘ ┴
doc └─────┘ └─────┘ └─────┘
73 (le_cSup : ∀s a, bdd_above s → a ∈ s → a ≤ Sup s)
id ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
src └───────┘ ┴ ┴
typ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
doc └───────┘
74 (cSup_le : ∀ s a, set.nonempty s → a ∈ upper_bounds s → Sup s ≤ a)
id ┴ ┴ └──────────┘ ┴ ┴ ┴ └──────────┘ ┴ └─┘ ┴ ┴ ┴
src └──────────┘ ┴ └──────────┘ ┴
typ ┴ ┴ └──────────┘ ┴ ┴ ┴ └──────────┘ ┴ └─┘ ┴ ┴ ┴
doc └──────────┘ └──────────┘
75 (cInf_le : ∀s a, bdd_below s → a ∈ s → Inf s ≤ a)
id ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
src └───────┘ ┴ ┴
typ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
doc └───────┘
76 (le_cInf : ∀s a, set.nonempty s → a ∈ lower_bounds s → a ≤ Inf s)
id ┴ ┴ └──────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ └─┘ ┴
src └──────────┘ ┴ └──────────┘ ┴
typ ┴ ┴ └──────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ └─┘ ┴
doc └──────────┘ └──────────┘
77
78 class conditionally_complete_linear_order (α : Type u)
id └──┘
typ └──┘
79 extends conditionally_complete_lattice α, decidable_linear_order α
id └────────────────────────────┘ ┴ └────────────────────┘ ┴
src └────────────────────────────┘ └────────────────────┘
typ └────────────────────────────┘ ┴ └────────────────────┘ ┴
doc └────────────────────────────┘
80
81 class conditionally_complete_linear_order_bot (α : Type u)
id ┴ └──┘
typ ┴ └──┘
82 extends conditionally_complete_lattice α, decidable_linear_order α, order_bot α :=
id └────────────────────────────┘ ┴ └────────────────────┘ ┴ └───────┘ ┴
src └────────────────────────────┘ └────────────────────┘ └───────┘
typ └────────────────────────────┘ ┴ └────────────────────┘ ┴ └───────┘ ┴
doc └────────────────────────────┘ └───────┘
83 (cSup_empty : Sup ∅ = ⊥)
id └─┘ ┴ ┴ ┴
src ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴
84 end prio
85
86 /- A complete lattice is a conditionally complete lattice, as there are no restrictions
87 on the properties of Inf and Sup in a complete lattice.-/
88
89 @[priority 100] -- see Note [lower instance priority]
90 instance conditionally_complete_lattice_of_complete_lattice [complete_lattice α]:
id └──────────────┘ ┴
src └──────────────┘
typ └──────────────┘ ┴
doc └──────────────┘
91 conditionally_complete_lattice α :=
id └────────────────────────────┘ ┴
src └────────────────────────────┘
typ └────────────────────────────┘ ┴
doc └────────────────────────────┘
92 { le_cSup := by intros; apply le_Sup; assumption,
id └────┘
src └────┘ └────┘└────┘ └────────┘
typ └────┘ └────┘└────┘ └────────┘
doc └────┘ └────┘ └────────┘
txt └────┘ └────┘ └────────┘
par └────┘ └────┘ └────────┘
pid ┴
st └───────────────────────────────┘
93 cSup_le := by intros; apply Sup_le; assumption,
id └────┘
src └────┘ └────┘└────┘ └────────┘
typ └────┘ └────┘└────┘ └────────┘
doc └────┘ └────┘ └────────┘
txt └────┘ └────┘ └────────┘
par └────┘ └────┘ └────────┘
pid ┴
st └───────────────────────────────┘
94 cInf_le := by intros; apply Inf_le; assumption,
id └────┘
src └────┘ └────┘└────┘ └────────┘
typ └────┘ └────┘└────┘ └────────┘
doc └────┘ └────┘ └────────┘
txt └────┘ └────┘ └────────┘
par └────┘ └────┘ └────────┘
pid ┴
st └───────────────────────────────┘
95 le_cInf := by intros; apply le_Inf; assumption,
id └────┘
src └────┘ └────┘└────┘ └────────┘
typ └────┘ └────┘└────┘ └────────┘
doc └────┘ └────┘ └────────┘
txt └────┘ └────┘ └────────┘
par └────┘ └────┘ └────────┘
pid ┴
st └───────────────────────────────┘
96 ..‹complete_lattice α› }
id ┴└──────────────┘ ┴┴
src ┴└──────────────┘ ┴
typ ┴└──────────────┘ ┴┴
doc ┴└──────────────┘ ┴
97
98 @[priority 100] -- see Note [lower instance priority]
99 instance conditionally_complete_linear_order_of_complete_linear_order [complete_linear_order α]:
id └───────────────────┘ ┴
src └───────────────────┘
typ └───────────────────┘ ┴
doc └───────────────────┘
100 conditionally_complete_linear_order α :=
id └─────────────────────────────────┘ ┴
src └─────────────────────────────────┘
typ └─────────────────────────────────┘ ┴
101 { ..lattice.conditionally_complete_lattice_of_complete_lattice, .. ‹complete_linear_order α› }
id └────────────────────────────────────────────────────────┘ ┴└───────────────────┘ ┴┴
src └────────────────────────────────────────────────────────┘ ┴└───────────────────┘ ┴
typ └────────────────────────────────────────────────────────┘ ┴└───────────────────┘ ┴┴
doc ┴└───────────────────┘ ┴
102
103 section conditionally_complete_lattice
104 variables [conditionally_complete_lattice α] {s t : set α} {a b : α}
id └────────────────────────────┘ └─┘
src └────────────────────────────┘ └─┘
typ └────────────────────────────┘ └─┘
doc └────────────────────────────┘
105
106 theorem le_cSup (h₁ : bdd_above s) (h₂ : a ∈ s) : a ≤ Sup s :=
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
src └───────┘ ┴ ┴ └─┘
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
doc └───────┘ └─┘
107 conditionally_complete_lattice.le_cSup s a h₁ h₂
id └────────────────────────────────────┘ ┴ ┴ └┘ └┘
src └────────────────────────────────────┘
typ └────────────────────────────────────┘ ┴ ┴ └┘ └┘
108
109 theorem cSup_le (h₁ : s.nonempty) (h₂ : ∀b∈s, b ≤ a) : Sup s ≤ a :=
id ┴└───────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
src └───────┘ ┴ ┴ └─┘ ┴
typ ┴└───────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
doc └───────┘ └─┘
110 conditionally_complete_lattice.cSup_le s a h₁ h₂
id └────────────────────────────────────┘ ┴ ┴ └┘ └┘
src └────────────────────────────────────┘
typ └────────────────────────────────────┘ ┴ ┴ └┘ └┘
111
112 theorem cInf_le (h₁ : bdd_below s) (h₂ : a ∈ s) : Inf s ≤ a :=
id └───────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
src └───────┘ ┴ └─┘ ┴
typ └───────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
doc └───────┘ └─┘
113 conditionally_complete_lattice.cInf_le s a h₁ h₂
id └────────────────────────────────────┘ ┴ ┴ └┘ └┘
src └────────────────────────────────────┘
typ └────────────────────────────────────┘ ┴ ┴ └┘ └┘
114
115 theorem le_cInf (h₁ : s.nonempty) (h₂ : ∀b∈s, a ≤ b) : a ≤ Inf s :=
id ┴└───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
src └───────┘ ┴ ┴ └─┘
typ ┴└───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
doc └───────┘ └─┘
116 conditionally_complete_lattice.le_cInf s a h₁ h₂
id └────────────────────────────────────┘ ┴ ┴ └┘ └┘
src └────────────────────────────────────┘
typ └────────────────────────────────────┘ ┴ ┴ └┘ └┘
117
118 theorem le_cSup_of_le (_ : bdd_above s) (hb : b ∈ s) (h : a ≤ b) : a ≤ Sup s :=
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
src └───────┘ ┴ ┴ ┴ └─┘
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
doc └───────┘ └─┘
119 le_trans h (le_cSup ‹bdd_above s› hb)
id └──────┘ ┴ └─────┘ ┴└───────┘ ┴┴ └┘
src └──────┘ └─────┘ ┴└───────┘ ┴
typ └──────┘ ┴ └─────┘ ┴└───────┘ ┴┴ └┘
doc ┴└───────┘ ┴
120
121 theorem cInf_le_of_le (_ : bdd_below s) (hb : b ∈ s) (h : b ≤ a) : Inf s ≤ a :=
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
src └───────┘ ┴ ┴ └─┘ ┴
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
doc └───────┘ └─┘
122 le_trans (cInf_le ‹bdd_below s› hb) h
id └──────┘ └─────┘ ┴└───────┘ ┴┴ └┘ ┴
src └──────┘ └─────┘ ┴└───────┘ ┴
typ └──────┘ └─────┘ ┴└───────┘ ┴┴ └┘ ┴
doc ┴└───────┘ ┴
123
124 theorem cSup_le_cSup (_ : bdd_above t) (_ : s.nonempty) (h : s ⊆ t) : Sup s ≤ Sup t :=
id └───────┘ ┴ ┴└───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src └───────┘ └───────┘ ┴ └─┘ ┴ └─┘
typ └───────┘ ┴ ┴└───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
doc └───────┘ └───────┘ └─┘ └─┘
125 cSup_le ‹_› (assume (a) (ha : a ∈ s), le_cSup ‹bdd_above t› (h ha))
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴└───────┘ ┴┴ ┴ └┘
src └─────┘ ┴ ┴ ┴ └─────┘ ┴└───────┘ ┴
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴└───────┘ ┴┴ ┴ └┘
doc ┴ ┴ ┴└───────┘ ┴
126
127 theorem cInf_le_cInf (_ : bdd_below t) (_ : s.nonempty) (h : s ⊆ t) : Inf t ≤ Inf s :=
id └───────┘ ┴ ┴└───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src └───────┘ └───────┘ ┴ └─┘ ┴ └─┘
typ └───────┘ ┴ ┴└───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
doc └───────┘ └───────┘ └─┘ └─┘
128 le_cInf ‹_› (assume (a) (ha : a ∈ s), cInf_le ‹bdd_below t› (h ha))
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴└───────┘ ┴┴ ┴ └┘
src └─────┘ ┴ ┴ ┴ └─────┘ ┴└───────┘ ┴
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴└───────┘ ┴┴ ┴ └┘
doc ┴ ┴ ┴└───────┘ ┴
129
130 theorem cSup_le_iff (_ : bdd_above s) (_ : s.nonempty) : Sup s ≤ a ↔ (∀b ∈ s, b ≤ a) :=
id └───────┘ ┴ ┴└───────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ └───────┘ └─┘ ┴ ┴ ┴
typ └───────┘ ┴ ┴└───────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘ └───────┘ └─┘
131 ⟨assume (_ : Sup s ≤ a) (b) (_ : b ∈ s),
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
132 le_trans (le_cSup ‹bdd_above s› ‹b ∈ s›) ‹Sup s ≤ a›,
id └──────┘ └─────┘ ┴└───────┘ ┴┴ ┴┴ ┴ ┴┴ ┴└─┘ ┴ ┴ ┴┴
src └──────┘ └─────┘ ┴└───────┘ ┴ ┴ ┴ ┴ ┴└─┘ ┴ ┴
typ └──────┘ └─────┘ ┴└───────┘ ┴┴ ┴┴ ┴ ┴┴ ┴└─┘ ┴ ┴ ┴┴
doc ┴└───────┘ ┴ ┴ ┴ ┴└─┘ ┴
133 cSup_le ‹_›⟩
id └─────┘ ┴ ┴
src └─────┘ ┴ ┴
typ └─────┘ ┴ ┴
doc ┴ ┴
134
135 theorem le_cInf_iff (_ : bdd_below s) (_ : s.nonempty) : a ≤ Inf s ↔ (∀b ∈ s, a ≤ b) :=
id └───────┘ ┴ ┴└───────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ └───────┘ ┴ └─┘ ┴ ┴
typ └───────┘ ┴ ┴└───────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘ └───────┘ └─┘
136 ⟨assume (_ : a ≤ Inf s) (b) (_ : b ∈ s),
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
doc └─┘
137 le_trans ‹a ≤ Inf s› (cInf_le ‹bdd_below s› ‹b ∈ s›),
id └──────┘ ┴┴ ┴ └─┘ ┴┴ └─────┘ ┴└───────┘ ┴┴ ┴┴ ┴ ┴┴
src └──────┘ ┴ ┴ └─┘ ┴ └─────┘ ┴└───────┘ ┴ ┴ ┴ ┴
typ └──────┘ ┴┴ ┴ └─┘ ┴┴ └─────┘ ┴└───────┘ ┴┴ ┴┴ ┴ ┴┴
doc ┴ └─┘ ┴ ┴└───────┘ ┴ ┴ ┴
138 le_cInf ‹_›⟩
id └─────┘ ┴ ┴
src └─────┘ ┴ ┴
typ └─────┘ ┴ ┴
doc ┴ ┴
139
140 lemma cSup_lower_bounds_eq_cInf {s : set α} (h : bdd_below s) (hs : s.nonempty) :
id └─┘ ┴ └───────┘ ┴ ┴└───────┘
src └─┘ └───────┘ └───────┘
typ └─┘ ┴ └───────┘ ┴ ┴└───────┘
doc └───────┘ └───────┘
141 Sup (lower_bounds s) = Inf s :=
id └─┘ └──────────┘ ┴ ┴ └─┘ ┴
src └─┘ └──────────┘ ┴ └─┘
typ └─┘ └──────────┘ ┴ ┴ └─┘ ┴
doc └─┘ └──────────┘ └─┘
142 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
143 (cSup_le h $ assume a ha, le_cInf hs ha)
id └─────┘ ┴ ┴ └┘ └─────┘ └┘ └┘
src └─────┘ └─────┘
typ └─────┘ ┴ ┴ └┘ └─────┘ └┘ └┘
144 (le_cSup (hs.mono $ λ a ha y hy, hy ha) $ assume x hx, cInf_le h hx)
id └─────┘ └┘└───┘ ┴ └┘ ┴ └┘ └┘ └┘ ┴ └┘ └─────┘ ┴ └┘
src └─────┘ └───┘ └─────┘
typ └─────┘ └┘└───┘ ┴ └┘ ┴ └┘ └┘ └┘ ┴ └┘ └─────┘ ┴ └┘
145
146 lemma cInf_upper_bounds_eq_cSup {s : set α} (h : bdd_above s) (hs : s.nonempty) :
id └─┘ ┴ └───────┘ ┴ ┴└───────┘
src └─┘ └───────┘ └───────┘
typ └─┘ ┴ └───────┘ ┴ ┴└───────┘
doc └───────┘ └───────┘
147 Inf (upper_bounds s) = Sup s :=
id └─┘ └──────────┘ ┴ ┴ └─┘ ┴
src └─┘ └──────────┘ ┴ └─┘
typ └─┘ └──────────┘ ┴ ┴ └─┘ ┴
doc └─┘ └──────────┘ └─┘
148 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
149 (cInf_le (hs.mono $ assume a ha y hy, hy ha) $ assume x hx, le_cSup h hx)
id └─────┘ └┘└───┘ ┴ └┘ ┴ └┘ └┘ └┘ ┴ └┘ └─────┘ ┴ └┘
src └─────┘ └───┘ └─────┘
typ └─────┘ └┘└───┘ ┴ └┘ ┴ └┘ └┘ └┘ ┴ └┘ └─────┘ ┴ └┘
150 (le_cInf h $ assume a ha, cSup_le hs ha)
id └─────┘ ┴ ┴ └┘ └─────┘ └┘ └┘
src └─────┘ └─────┘
typ └─────┘ ┴ ┴ └┘ └─────┘ └┘ └┘
151
152 /--Introduction rule to prove that b is the supremum of s: it suffices to check that b
153 is larger than all elements of s, and that this is not the case of any w<b.-/
154 theorem cSup_intro (_ : s.nonempty) (_ : ∀a∈s, a ≤ b) (H : ∀w, w < b → (∃a∈s, w < a)) : Sup s = b :=
id ┴└───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
src └───────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
typ ┴└───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
doc └───────┘ └─┘
155 have bdd_above s := ⟨b, by assumption⟩,
id └───────┘ ┴ ┴
src └───────┘ └────────┘
typ └───────┘ ┴ ┴ └────────┘
doc └───────┘ └────────┘
txt └────────┘
par └────────┘
st └─────────┘
156 have (Sup s < b) ∨ (Sup s = b) := lt_or_eq_of_le (cSup_le ‹_› ‹∀a∈s, a ≤ b›),
id └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └────────────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
src └─┘ ┴ ┴ └─┘ ┴ └────────────┘ └─────┘ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └────────────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
doc └─┘ └─┘ ┴ ┴ ┴ ┴
157 have ¬(Sup s < b) :=
id ┴ └─┘ ┴ ┴ ┴
src ┴ └─┘ ┴
typ ┴ └─┘ ┴ ┴ ┴
doc └─┘
158 assume: Sup s < b,
id └─┘ ┴ ┴ ┴
src └─┘ ┴
typ └─┘ ┴ ┴ ┴
doc └─┘
159 let ⟨a, _, _⟩ := (H (Sup s) ‹Sup s < b›) in /- a ∈ s, Sup s < a-/
id └─┘ ┴ ┴ └─┘ ┴ ┴└─┘ ┴ ┴ ┴┴
src └─┘ ┴└─┘ ┴ ┴
typ └─┘ ┴ ┴ └─┘ ┴ ┴└─┘ ┴ ┴ ┴┴
doc └─┘ ┴└─┘ ┴
160 have Sup s < Sup s := lt_of_lt_of_le ‹Sup s < a› (le_cSup ‹bdd_above s› ‹a ∈ s›),
id └─┘ ┴ ┴ └─┘ ┴ └────────────┘ ┴└─┘ ┴ ┴ ┴ └─────┘ ┴└───────┘ ┴┴ ┴ ┴ ┴┴
src └─┘ ┴ └─┘ └────────────┘ ┴└─┘ ┴ ┴ └─────┘ ┴└───────┘ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ └─┘ ┴ └────────────┘ ┴└─┘ ┴ ┴ ┴ └─────┘ ┴└───────┘ ┴┴ ┴ ┴ ┴┴
doc └─┘ └─┘ ┴└─┘ ┴ ┴└───────┘ ┴ ┴ ┴
161 show false, by finish [lt_irrefl (Sup s)],
id └───┘ └───────┘ └─┘ ┴
src └───┘ └──────┘└───────┘┴ └─┘┴ └┘
typ └───┘ └──────┘└───────┘┴ └─┘┴┴└┘
doc └──────┘ ┴ └─┘┴ └┘
txt └──────┘ ┴ ┴ └┘
par └──────┘ ┴ ┴ └┘
pid └┘ ┴ ┴ └┘
st └─────────────────────────┘
162 show Sup s = b, by finish
id └─┘ ┴ ┴ ┴
src └─┘ ┴ └──────
typ └─┘ ┴ ┴ ┴ └──────
doc └─┘ └──────
txt └──────
par └──────
pid └
st └───────
163
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
164 /--Introduction rule to prove that b is the infimum of s: it suffices to check that b
165 is smaller than all elements of s, and that this is not the case of any w>b.-/
166 theorem cInf_intro (_ : s.nonempty) (_ : ∀a∈s, b ≤ a) (H : ∀w, b < w → (∃a∈s, a < w)) : Inf s = b :=
id ┴└───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
src └───────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
typ ┴└───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
doc └───────┘ └─┘
167 have bdd_below s := ⟨b, by assumption⟩,
id └───────┘ ┴ ┴
src └───────┘ └────────┘
typ └───────┘ ┴ ┴ └────────┘
doc └───────┘ └────────┘
txt └────────┘
par └────────┘
st └─────────┘
168 have (b < Inf s) ∨ (b = Inf s) := lt_or_eq_of_le (le_cInf ‹_› ‹∀a∈s, b ≤ a›),
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ └────────────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
src ┴ └─┘ ┴ ┴ └─┘ └────────────┘ └─────┘ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ └────────────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
doc └─┘ └─┘ ┴ ┴ ┴ ┴
169 have ¬(b < Inf s) :=
id ┴ ┴ ┴ └─┘ ┴
src ┴ ┴ └─┘
typ ┴ ┴ ┴ └─┘ ┴
doc └─┘
170 assume: b < Inf s,
id ┴ ┴ └─┘ ┴
src ┴ └─┘
typ ┴ ┴ └─┘ ┴
doc └─┘
171 let ⟨a, _, _⟩ := (H (Inf s) ‹b < Inf s›) in /- a ∈ s, a < Inf s-/
id └─┘ ┴ ┴ └─┘ ┴ ┴┴ ┴ └─┘ ┴┴
src └─┘ ┴ ┴ └─┘ ┴
typ └─┘ ┴ ┴ └─┘ ┴ ┴┴ ┴ └─┘ ┴┴
doc └─┘ ┴ └─┘ ┴
172 have Inf s < Inf s := lt_of_le_of_lt (cInf_le ‹bdd_below s› ‹a ∈ s›) ‹a < Inf s› ,
id └─┘ ┴ ┴ └─┘ ┴ └────────────┘ └─────┘ ┴└───────┘ ┴┴ ┴ ┴ ┴┴ ┴ ┴ └─┘ ┴┴
src └─┘ ┴ └─┘ └────────────┘ └─────┘ ┴└───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
typ └─┘ ┴ ┴ └─┘ ┴ └────────────┘ └─────┘ ┴└───────┘ ┴┴ ┴ ┴ ┴┴ ┴ ┴ └─┘ ┴┴
doc └─┘ └─┘ ┴└───────┘ ┴ ┴ ┴ ┴ └─┘ ┴
173 show false, by finish [lt_irrefl (Inf s)],
id └───┘ └───────┘ └─┘ ┴
src └───┘ └──────┘└───────┘┴ └─┘┴ └┘
typ └───┘ └──────┘└───────┘┴ └─┘┴┴└┘
doc └──────┘ ┴ └─┘┴ └┘
txt └──────┘ ┴ ┴ └┘
par └──────┘ ┴ ┴ └┘
pid └┘ ┴ ┴ └┘
st └─────────────────────────┘
174 show Inf s = b, by finish
id └─┘ ┴ ┴ ┴
src └─┘ ┴ └──────
typ └─┘ ┴ ┴ ┴ └──────
doc └─┘ └──────
txt └──────
par └──────
pid └
st └───────
175
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
176 /--When an element a of a set s is larger than all other elements of the set, it is Sup s-/
177 theorem cSup_of_mem_of_le (_ : a ∈ s) (_ : ∀w∈s, w ≤ a) : Sup s = a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
src ┴ ┴ └─┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
doc └─┘
178 have bdd_above s := ⟨a, by assumption⟩,
id └───────┘ ┴ ┴
src └───────┘ └────────┘
typ └───────┘ ┴ ┴ └────────┘
doc └───────┘ └────────┘
txt └────────┘
par └────────┘
st └─────────┘
179 have A : a ≤ Sup s := le_cSup ‹bdd_above s› ‹a ∈ s›,
id ┴ ┴ └─┘ ┴ └─────┘ ┴└───────┘ ┴┴ ┴┴ ┴ ┴┴
src ┴ └─┘ └─────┘ ┴└───────┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └─┘ ┴ └─────┘ ┴└───────┘ ┴┴ ┴┴ ┴ ┴┴
doc └─┘ ┴└───────┘ ┴ ┴ ┴
180 have B : Sup s ≤ a := cSup_le ⟨a, ‹_›⟩ ‹∀w∈s, w ≤ a›,
id └─┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
src └─┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
doc └─┘ ┴ ┴ ┴ ┴
181 le_antisymm B A
id └─────────┘ ┴ ┴
src └─────────┘
typ └─────────┘ ┴ ┴
182
183 /--When an element a of a set s is smaller than all other elements of the set, it is Inf s-/
184 theorem cInf_of_mem_of_le (_ : a ∈ s) (_ : ∀w∈s, a ≤ w) : Inf s = a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
src ┴ ┴ └─┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
doc └─┘
185 have bdd_below s := ⟨a, by assumption⟩,
id └───────┘ ┴ ┴
src └───────┘ └────────┘
typ └───────┘ ┴ ┴ └────────┘
doc └───────┘ └────────┘
txt └────────┘
par └────────┘
st └─────────┘
186 have A : Inf s ≤ a := cInf_le ‹bdd_below s› ‹a ∈ s›,
id └─┘ ┴ ┴ ┴ └─────┘ ┴└───────┘ ┴┴ ┴┴ ┴ ┴┴
src └─┘ ┴ └─────┘ ┴└───────┘ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ └─────┘ ┴└───────┘ ┴┴ ┴┴ ┴ ┴┴
doc └─┘ ┴└───────┘ ┴ ┴ ┴
187 have B : a ≤ Inf s := le_cInf ⟨a, ‹_›⟩ ‹∀w∈s, a ≤ w›,
id ┴ ┴ └─┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
src ┴ └─┘ └─────┘ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └─┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
doc └─┘ ┴ ┴ ┴ ┴
188 le_antisymm A B
id └─────────┘ ┴ ┴
src └─────────┘
typ └─────────┘ ┴ ┴
189
190 /--b < Sup s when there is an element a in s with b < a, when s is bounded above.
191 This is essentially an iff, except that the assumptions for the two implications are
192 slightly different (one needs boundedness above for one direction, nonemptiness and linear
193 order for the other one), so we formulate separately the two implications, contrary to
194 the complete_lattice case.-/
195 lemma lt_cSup_of_lt (_ : bdd_above s) (_ : a ∈ s) (_ : b < a) : b < Sup s :=
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
src └───────┘ ┴ ┴ ┴ └─┘
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
doc └───────┘ └─┘
196 lt_of_lt_of_le ‹b < a› (le_cSup ‹bdd_above s› ‹a ∈ s›)
id └────────────┘ ┴┴ ┴ ┴┴ └─────┘ ┴└───────┘ ┴┴ ┴┴ ┴ ┴┴
src └────────────┘ ┴ ┴ ┴ └─────┘ ┴└───────┘ ┴ ┴ ┴ ┴
typ └────────────┘ ┴┴ ┴ ┴┴ └─────┘ ┴└───────┘ ┴┴ ┴┴ ┴ ┴┴
doc ┴ ┴ ┴└───────┘ ┴ ┴ ┴
197
198 /--Inf s < b when there is an element a in s with a < b, when s is bounded below.
199 This is essentially an iff, except that the assumptions for the two implications are
200 slightly different (one needs boundedness below for one direction, nonemptiness and linear
201 order for the other one), so we formulate separately the two implications, contrary to
202 the complete_lattice case.-/
203
204 lemma cInf_lt_of_lt (_ : bdd_below s) (_ : a ∈ s) (_ : a < b) : Inf s < b :=
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
src └───────┘ ┴ ┴ └─┘ ┴
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
doc └───────┘ └─┘
205 lt_of_le_of_lt (cInf_le ‹bdd_below s› ‹a ∈ s›) ‹a < b›
id └────────────┘ └─────┘ ┴└───────┘ ┴┴ ┴┴ ┴ ┴┴ ┴┴ ┴ ┴┴
src └────────────┘ └─────┘ ┴└───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └────────────┘ └─────┘ ┴└───────┘ ┴┴ ┴┴ ┴ ┴┴ ┴┴ ┴ ┴┴
doc ┴└───────┘ ┴ ┴ ┴ ┴ ┴
206
207 /--The supremum of a singleton is the element of the singleton-/
208 @[simp] theorem cSup_singleton (a : α) : Sup {a} = a :=
id ┴ └─┘ ┴┴ ┴ ┴
src └─┘ ┴ ┴
typ ┴ └─┘ ┴┴ ┴ ┴
doc └──┘ └─┘
209 cSup_of_mem_of_le (mem_singleton a)
id └───────────────┘ └───────────┘ ┴
src └───────────────┘ └───────────┘
typ └───────────────┘ └───────────┘ ┴
doc └───────────────┘
210 (λ b hb, set.eq_of_mem_singleton hb ▸ le_refl b)
id ┴ └┘ └─────────────────────┘ └┘ ┴ └─────┘ ┴
src └─────────────────────┘ ┴ └─────┘
typ ┴ └┘ └─────────────────────┘ └┘ ┴ └─────┘ ┴
211
212 /--The infimum of a singleton is the element of the singleton-/
213 @[simp] theorem cInf_singleton (a : α) : Inf {a} = a :=
id ┴ └─┘ ┴┴ ┴ ┴
src └─┘ ┴ ┴
typ ┴ └─┘ ┴┴ ┴ ┴
doc └──┘ └─┘
214 cInf_of_mem_of_le (mem_singleton a)
id └───────────────┘ └───────────┘ ┴
src └───────────────┘ └───────────┘
typ └───────────────┘ └───────────┘ ┴
doc └───────────────┘
215 (λ b hb, set.eq_of_mem_singleton hb ▸ le_refl b)
id ┴ └┘ └─────────────────────┘ └┘ ┴ └─────┘ ┴
src └─────────────────────┘ ┴ └─────┘
typ ┴ └┘ └─────────────────────┘ └┘ ┴ └─────┘ ┴
216
217 /--If a set is bounded below and above, and nonempty, its infimum is less than or equal to
218 its supremum.-/
219 theorem cInf_le_cSup (_ : bdd_below s) (_ : bdd_above s) (_ : s.nonempty) : Inf s ≤ Sup s :=
id └───────┘ ┴ └───────┘ ┴ ┴└───────┘ └─┘ ┴ ┴ └─┘ ┴
src └───────┘ └───────┘ └───────┘ └─┘ ┴ └─┘
typ └───────┘ ┴ └───────┘ ┴ ┴└───────┘ └─┘ ┴ ┴ └─┘ ┴
doc └───────┘ └───────┘ └───────┘ └─┘ └─┘
220 let ⟨w, hw⟩ := ‹s.nonempty› in /-hw : w ∈ s-/
id └─┘ ┴ ┴┴└───────┘┴
src ┴ └───────┘┴
typ └─┘ ┴ ┴┴└───────┘┴
doc ┴ └───────┘┴
221 have Inf s ≤ w := cInf_le ‹bdd_below s› ‹w ∈ s›,
id └─┘ ┴ ┴ └─────┘ ┴└───────┘ ┴┴ ┴ ┴ ┴┴
src └─┘ ┴ └─────┘ ┴└───────┘ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ └─────┘ ┴└───────┘ ┴┴ ┴ ┴ ┴┴
doc └─┘ ┴└───────┘ ┴ ┴ ┴
222 have w ≤ Sup s := le_cSup ‹bdd_above s› ‹w ∈ s›,
id ┴ └─┘ ┴ └─────┘ ┴└───────┘ ┴┴ ┴ ┴ ┴┴
src ┴ └─┘ └─────┘ ┴└───────┘ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴ └─────┘ ┴└───────┘ ┴┴ ┴ ┴ ┴┴
doc └─┘ ┴└───────┘ ┴ ┴ ┴
223 le_trans ‹Inf s ≤ w› ‹w ≤ Sup s›
id └──────┘ ┴└─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴┴
src └──────┘ ┴└─┘ ┴ ┴ ┴ ┴ └─┘ ┴
typ └──────┘ ┴└─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴┴
doc ┴└─┘ ┴ ┴ └─┘ ┴
224
225 /--The sup of a union of two sets is the max of the suprema of each subset, under the assumptions
226 that all sets are bounded above and nonempty.-/
227 theorem cSup_union (_ : bdd_above s) (sne : s.nonempty) (_ : bdd_above t) (tne : t.nonempty) :
id └───────┘ ┴ ┴└───────┘ └───────┘ ┴ ┴└───────┘
src └───────┘ └───────┘ └───────┘ └───────┘
typ └───────┘ ┴ ┴└───────┘ └───────┘ ┴ ┴└───────┘
doc └───────┘ └───────┘ └───────┘ └───────┘
228 Sup (s ∪ t) = Sup s ⊔ Sup t :=
id └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src └─┘ ┴ ┴ └─┘ ┴ └─┘
typ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
doc └─┘ └─┘ └─┘
229 have A : Sup (s ∪ t) ≤ Sup s ⊔ Sup t :=
id └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src └─┘ ┴ ┴ └─┘ ┴ └─┘
typ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
doc └─┘ └─┘ └─┘
230 have (s ∪ t).nonempty := sne.inl,
id ┴ ┴ ┴ └──────┘ └─┘└──┘
src ┴ └──────┘ └──┘
typ ┴ ┴ ┴ └──────┘ └─┘└──┘
doc └──────┘
231 have F : ∀b∈ s∪t, b ≤ Sup s ⊔ Sup t :=
id ┴ ┴┴┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src ┴ ┴ └─┘ ┴ └─┘
typ ┴ ┴┴┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
doc └─┘ └─┘
232 begin
st └─────
233 intros,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
st ───────────┘└─
234 cases H,
id ┴
src └────┘
typ └────┘┴
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────┘└─
235 apply le_trans (le_cSup ‹bdd_above s› ‹b ∈ s›) _, simp only [lattice.le_sup_left],
id └──────┘ └─────┘ ┴└───────┘ ┴ ┴ ┴ ┴ └─────────────────┘
src └────┘└──────┘┴ └─────┘┴┴└───────┘┴ ┴┴ ┴┴┴ └─┘ └─────────┘└─────────────────┘┴
typ └────┘└──────┘┴ └─────┘┴┴└───────┘┴ ┴┴ ┴┴┴┴┴ └─┘ └─────────┘└─────────────────┘┴
doc └────┘ ┴ ┴┴└───────┘┴ ┴┴ ┴ ┴ └─┘ └─────────┘ ┴
txt └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─────────┘ ┴
par └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─────────┘ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└──┘└┘ ┴
st ─────────────────────────────────────────────────────┘└───────────────────────────────┘└─
236 apply le_trans (le_cSup ‹bdd_above t› ‹b ∈ t›) _, simp only [lattice.le_sup_right]
id └──────┘ └─────┘ └───────┘ ┴ ┴ └──────────────────┘
src └────┘└──────┘┴ └─────┘┴ └───────┘┴ ┴ ┴ ┴ └─┘ └─────────┘└──────────────────┘└─
typ └────┘└──────┘┴ └─────┘┴ └───────┘┴ ┴ ┴┴ ┴┴ └─┘ └─────────┘└──────────────────┘└─
doc └────┘ ┴ ┴ └───────┘┴ ┴ ┴ ┴ └─┘ └─────────┘ └─
txt └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─────────┘ └─
par └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─────────┘ └─
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└──┘└┘ ┴└
st ─────────────────────────────────────────────────────┘└──────────────────────────────────
237 end,
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘
238 cSup_le this F,
id └─────┘ └──┘ ┴
src └─────┘
typ └─────┘ └──┘ ┴
239 have B : Sup s ⊔ Sup t ≤ Sup (s ∪ t) :=
id └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴
src └─┘ ┴ └─┘ ┴ └─┘ ┴
typ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴
doc └─┘ └─┘ └─┘
240 have Sup s ≤ Sup (s ∪ t),
id └─┘ ┴ ┴ └─┘ ┴ ┴ ┴
src └─┘ ┴ └─┘ ┴
typ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴
doc └─┘ └─┘
241 from cSup_le_cSup (bdd_above_union.2 ⟨‹_›, ‹_›⟩) sne (set.subset_union_left _ _),
id └──────────┘ └─────────────┘┴ ┴ ┴ ┴ ┴ └─┘ └───────────────────┘
src └──────────┘ └─────────────┘┴ ┴ ┴ ┴ ┴ └───────────────────┘
typ └──────────┘ └─────────────┘┴ ┴ ┴ ┴ ┴ └─┘ └───────────────────┘
doc └─────────────┘ ┴ ┴ ┴ ┴
242 have Sup t ≤ Sup (s ∪ t),
id └─┘ ┴ ┴ └─┘ ┴ ┴ ┴
src └─┘ ┴ └─┘ ┴
typ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴
doc └─┘ └─┘
243 from cSup_le_cSup (bdd_above_union.2 ⟨‹_›, ‹_›⟩) tne (set.subset_union_right _ _),
id └──────────┘ └─────────────┘┴ ┴ ┴ ┴ ┴ └─┘ └────────────────────┘
src └──────────┘ └─────────────┘┴ ┴ ┴ ┴ ┴ └────────────────────┘
typ └──────────┘ └─────────────┘┴ ┴ ┴ ┴ ┴ └─┘ └────────────────────┘
doc └─────────────┘ ┴ ┴ ┴ ┴
244 by simp only [lattice.sup_le_iff]; split; assumption,
id └────────────────┘
src └─────────┘└────────────────┘┴ └───┘ └────────┘
typ └─────────┘└────────────────┘┴ └───┘ └────────┘
doc └─────────┘ ┴ └───┘ └────────┘
txt └─────────┘ ┴ └───┘ └────────┘
par └─────────┘ ┴ └───┘ └────────┘
pid ┴└──┘└┘ ┴
st └────────────────────────────────────────────────┘
245 le_antisymm A B
id └─────────┘ ┴ ┴
src └─────────┘
typ └─────────┘ ┴ ┴
246
247 /--The inf of a union of two sets is the min of the infima of each subset, under the assumptions
248 that all sets are bounded below and nonempty.-/
249 theorem cInf_union (_ : bdd_below s) (sne : s.nonempty) (_ : bdd_below t) (tne : t.nonempty) :
id └───────┘ ┴ ┴└───────┘ └───────┘ ┴ ┴└───────┘
src └───────┘ └───────┘ └───────┘ └───────┘
typ └───────┘ ┴ ┴└───────┘ └───────┘ ┴ ┴└───────┘
doc └───────┘ └───────┘ └───────┘ └───────┘
250 Inf (s ∪ t) = Inf s ⊓ Inf t :=
id └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src └─┘ ┴ ┴ └─┘ ┴ └─┘
typ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
doc └─┘ └─┘ └─┘
251 have A : Inf s ⊓ Inf t ≤ Inf (s ∪ t) :=
id └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴
src └─┘ ┴ └─┘ ┴ └─┘ ┴
typ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴
doc └─┘ └─┘ └─┘
252 have (s ∪ t).nonempty, from sne.inl,
id ┴ ┴ ┴ └──────┘ └─┘└──┘
src ┴ └──────┘ └──┘
typ ┴ ┴ ┴ └──────┘ └─┘└──┘
doc └──────┘
253 have F : ∀b∈ s∪t, Inf s ⊓ Inf t ≤ b :=
id ┴ ┴┴┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴
src ┴ └─┘ ┴ └─┘ ┴
typ ┴ ┴┴┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴
doc └─┘ └─┘
254 begin
st └─────
255 intros,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
st ───────────┘└─
256 cases H,
id ┴
src └────┘
typ └────┘┴
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────┘└─
257 apply le_trans _ (cInf_le ‹bdd_below s› ‹b ∈ s›), simp only [lattice.inf_le_left],
id └──────┘ └─────┘ ┴└───────┘ ┴ ┴ ┴ ┴ └─────────────────┘
src └────┘└──────┘└─┘ └─────┘┴┴└───────┘┴ ┴┴ ┴┴┴ ┴ └─────────┘└─────────────────┘┴
typ └────┘└──────┘└─┘ └─────┘┴┴└───────┘┴ ┴┴ ┴┴┴┴┴ ┴ └─────────┘└─────────────────┘┴
doc └────┘ └─┘ ┴┴└───────┘┴ ┴┴ ┴ ┴ ┴ └─────────┘ ┴
txt └────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘ ┴
par └────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘ ┴
pid ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘└┘ ┴
st ─────────────────────────────────────────────────────┘└───────────────────────────────┘└─
258 apply le_trans _ (cInf_le ‹bdd_below t› ‹b ∈ t›), simp only [lattice.inf_le_right]
id └──────┘ └─────┘ └───────┘ ┴ ┴ └──────────────────┘
src └────┘└──────┘└─┘ └─────┘┴ └───────┘┴ ┴ ┴ ┴ ┴ └─────────┘└──────────────────┘└─
typ └────┘└──────┘└─┘ └─────┘┴ └───────┘┴ ┴ ┴┴ ┴┴ ┴ └─────────┘└──────────────────┘└─
doc └────┘ └─┘ ┴ └───────┘┴ ┴ ┴ ┴ ┴ └─────────┘ └─
txt └────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘ └─
par └────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘ └─
pid ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘└┘ ┴└
st ─────────────────────────────────────────────────────┘└──────────────────────────────────
259 end,
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘
260 le_cInf this F,
id └─────┘ └──┘ ┴
src └─────┘
typ └─────┘ └──┘ ┴
261 have B : Inf (s ∪ t) ≤ Inf s ⊓ Inf t :=
id └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src └─┘ ┴ ┴ └─┘ ┴ └─┘
typ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
doc └─┘ └─┘ └─┘
262 have Inf (s ∪ t) ≤ Inf s,
id └─┘ ┴ ┴ ┴ ┴ └─┘ ┴
src └─┘ ┴ ┴ └─┘
typ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴
doc └─┘ └─┘
263 from cInf_le_cInf (bdd_below_union.2 ⟨‹_›, ‹_›⟩) sne (set.subset_union_left _ _),
id └──────────┘ └─────────────┘┴ ┴ ┴ ┴ ┴ └─┘ └───────────────────┘
src └──────────┘ └─────────────┘┴ ┴ ┴ ┴ ┴ └───────────────────┘
typ └──────────┘ └─────────────┘┴ ┴ ┴ ┴ ┴ └─┘ └───────────────────┘
doc └─────────────┘ ┴ ┴ ┴ ┴
264 have Inf (s ∪ t) ≤ Inf t,
id └─┘ ┴ ┴ ┴ ┴ └─┘ ┴
src └─┘ ┴ ┴ └─┘
typ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴
doc └─┘ └─┘
265 from cInf_le_cInf (bdd_below_union.2 ⟨‹_›, ‹_›⟩) tne (set.subset_union_right _ _),
id └──────────┘ └─────────────┘┴ ┴ ┴ ┴ ┴ └─┘ └────────────────────┘
src └──────────┘ └─────────────┘┴ ┴ ┴ ┴ ┴ └────────────────────┘
typ └──────────┘ └─────────────┘┴ ┴ ┴ ┴ ┴ └─┘ └────────────────────┘
doc └─────────────┘ ┴ ┴ ┴ ┴
266 by simp only [lattice.le_inf_iff]; split; assumption; assumption,
id └────────────────┘
src └─────────┘└────────────────┘┴ └───┘ └────────┘ └────────┘
typ └─────────┘└────────────────┘┴ └───┘ └────────┘ └────────┘
doc └─────────┘ ┴ └───┘ └────────┘ └────────┘
txt └─────────┘ ┴ └───┘ └────────┘ └────────┘
par └─────────┘ ┴ └───┘ └────────┘ └────────┘
pid ┴└──┘└┘ ┴
st └────────────────────────────────────────────────────────────┘
267 le_antisymm B A
id └─────────┘ ┴ ┴
src └─────────┘
typ └─────────┘ ┴ ┴
268
269 /--The supremum of an intersection of two sets is bounded by the minimum of the suprema of each
270 set, if all sets are bounded above and nonempty.-/
271 theorem cSup_inter_le (_ : bdd_above s) (_ : bdd_above t) (hst : (s ∩ t).nonempty) :
id └───────┘ ┴ └───────┘ ┴ ┴ ┴ ┴ └──────┘
src └───────┘ └───────┘ ┴ └──────┘
typ └───────┘ ┴ └───────┘ ┴ ┴ ┴ ┴ └──────┘
doc └───────┘ └───────┘ └──────┘
272 Sup (s ∩ t) ≤ Sup s ⊓ Sup t :=
id └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src └─┘ ┴ ┴ └─┘ ┴ └─┘
typ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
doc └─┘ └─┘ └─┘
273 begin
st └─────
274 apply cSup_le hst, simp only [lattice.le_inf_iff, and_imp, set.mem_inter_eq], intros b _ _, split,
id └─────┘ └─┘ └────────────────┘ └─────┘ └──────────────┘
src └────┘└─────┘┴ └─────────┘└────────────────┘└┘└─────┘└┘└──────────────┘┴ └──────────┘ └───┘
typ └────┘└─────┘┴└─┘ └─────────┘└────────────────┘└┘└─────┘└┘└──────────────┘┴ └──────────┘ └───┘
doc └────┘ ┴ └─────────┘ └┘ └┘ ┴ └──────────┘ └───┘
txt └────┘ ┴ └─────────┘ └┘ └┘ ┴ └──────────┘ └───┘
par └────┘ ┴ └─────────┘ └┘ └┘ ┴ └──────────┘ └───┘
pid ┴ ┴ ┴└──┘└┘ └┘ └┘ ┴ └────┘
st ──────────────────┘└─────────────────────────────────────────────────────────┘└────────────┘└─────┘└─
275 apply le_cSup ‹bdd_above s› ‹b ∈ s›,
id └─────┘ ┴└───────┘ ┴ ┴ ┴ ┴
src └────┘└─────┘┴┴└───────┘┴ ┴┴ ┴┴┴
typ └────┘└─────┘┴┴└───────┘┴ ┴┴ ┴┴┴┴┴
doc └────┘ ┴┴└───────┘┴ ┴┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────┘└─
276 apply le_cSup ‹bdd_above t› ‹b ∈ t›
id └─────┘ └───────┘ ┴ ┴
src └────┘└─────┘┴ └───────┘┴ ┴ ┴ ┴ ┴
typ └────┘└─────┘┴ └───────┘┴ ┴ ┴┴ ┴┴ ┴
doc └────┘ ┴ └───────┘┴ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────┘
277 end
st └─┘
278
279 /--The infimum of an intersection of two sets is bounded below by the maximum of the
280 infima of each set, if all sets are bounded below and nonempty.-/
281 theorem le_cInf_inter (_ : bdd_below s) (_ : bdd_below t) (hst : (s ∩ t).nonempty) :
id └───────┘ ┴ └───────┘ ┴ ┴ ┴ ┴ └──────┘
src └───────┘ └───────┘ ┴ └──────┘
typ └───────┘ ┴ └───────┘ ┴ ┴ ┴ ┴ └──────┘
doc └───────┘ └───────┘ └──────┘
282 Inf s ⊔ Inf t ≤ Inf (s ∩ t) :=
id └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴
src └─┘ ┴ └─┘ ┴ └─┘ ┴
typ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴
doc └─┘ └─┘ └─┘
283 begin
st └─────
284 apply le_cInf hst, simp only [and_imp, set.mem_inter_eq, lattice.sup_le_iff], intros b _ _, split,
id └─────┘ └─┘ └─────┘ └──────────────┘ └────────────────┘
src └────┘└─────┘┴ └─────────┘└─────┘└┘└──────────────┘└┘└────────────────┘┴ └──────────┘ └───┘
typ └────┘└─────┘┴└─┘ └─────────┘└─────┘└┘└──────────────┘└┘└────────────────┘┴ └──────────┘ └───┘
doc └────┘ ┴ └─────────┘ └┘ └┘ ┴ └──────────┘ └───┘
txt └────┘ ┴ └─────────┘ └┘ └┘ ┴ └──────────┘ └───┘
par └────┘ ┴ └─────────┘ └┘ └┘ ┴ └──────────┘ └───┘
pid ┴ ┴ ┴└──┘└┘ └┘ └┘ ┴ └────┘
st ──────────────────┘└─────────────────────────────────────────────────────────┘└────────────┘└─────┘└─
285 apply cInf_le ‹bdd_below s› ‹b ∈ s›,
id └─────┘ ┴└───────┘ ┴ ┴ ┴ ┴
src └────┘└─────┘┴┴└───────┘┴ ┴┴ ┴┴┴
typ └────┘└─────┘┴┴└───────┘┴ ┴┴ ┴┴┴┴┴
doc └────┘ ┴┴└───────┘┴ ┴┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────┘└─
286 apply cInf_le ‹bdd_below t› ‹b ∈ t›
id └─────┘ └───────┘ ┴ ┴
src └────┘└─────┘┴ └───────┘┴ ┴ ┴ ┴ ┴
typ └────┘└─────┘┴ └───────┘┴ ┴ ┴┴ ┴┴ ┴
doc └────┘ ┴ └───────┘┴ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────┘
287 end
st └─┘
288
289 /-- The supremum of insert a s is the maximum of a and the supremum of s, if s is
290 nonempty and bounded above.-/
291 theorem cSup_insert (_ : bdd_above s) (sne : s.nonempty) : Sup (insert a s) = a ⊔ Sup s :=
id └───────┘ ┴ ┴└───────┘ └─┘ └────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
src └───────┘ └───────┘ └─┘ └────┘ ┴ ┴ └─┘
typ └───────┘ ┴ ┴└───────┘ └─┘ └────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
doc └───────┘ └───────┘ └─┘ └─┘
292 calc Sup (insert a s)
id └─┘ └────┘ ┴ ┴
src └─┘ └────┘
typ └─┘ └────┘ ┴ ┴
doc └─┘
293 = Sup ({a} ∪ s) : by rw [insert_eq]
id └─┘ ┴┴ ┴ ┴ └───────┘
src └─┘ ┴ ┴ └──┘└───────┘└─
typ └─┘ ┴┴ ┴ ┴ └──┘└───────┘└─
doc └─┘ └──┘ └─
txt └──┘ └─
par └──┘ └─
pid └┘ ┴└
st └────────────┘┴└
294 ... = Sup {a} ⊔ Sup s : by apply cSup_union _ _ ‹bdd_above s› sne; simp only [ne.def, not_false_iff, set.singleton_nonempty, bdd_above_singleton]
id └─┘ ┴┴ ┴ └─┘ ┴ └────────┘ ┴└───────┘ ┴┴ └─┘ └────┘ └───────────┘ └────────────────────┘ └─────────────────┘
src ───┘ └─┘ ┴ ┴ └─┘ └────┘└────────┘└───┘┴└───────┘┴ ┴┴ └─────────┘└────┘└┘└───────────┘└┘└────────────────────┘└┘└─────────────────┘└─
typ ───┘ └─┘ ┴┴ ┴ └─┘ ┴ └────┘└────────┘└───┘┴└───────┘┴┴┴┴└─┘ └─────────┘└────┘└┘└───────────┘└┘└────────────────────┘└┘└─────────────────┘└─
doc ───┘ └─┘ └─┘ └────┘└────────┘└───┘┴└───────┘┴ ┴┴ └─────────┘ └┘ └┘ └┘ └─
txt ───┘ └────┘ └───┘ ┴ ┴ └─────────┘ └┘ └┘ └┘ └─
par ───┘ └────┘ └───┘ ┴ ┴ └─────────┘ └┘ └┘ └┘ └─
pid ───┘ ┴ └───┘ ┴ ┴ ┴└──┘└┘ └┘ └┘ └┘ ┴└
st ───┘ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
295 ... = a ⊔ Sup s : by simp only [eq_self_iff_true, lattice.cSup_singleton]
id ┴ ┴ └─┘ ┴ └──────────────┘ └────────────────────┘
src ───┘ ┴ └─┘ └─────────┘└──────────────┘└┘└────────────────────┘└─
typ ───┘ ┴ ┴ └─┘ ┴ └─────────┘└──────────────┘└┘└────────────────────┘└─
doc ───┘ └─┘ └─────────┘ └┘└────────────────────┘└─
txt ───┘ └─────────┘ └┘ └─
par ───┘ └─────────┘ └┘ └─
pid ───┘ ┴└──┘└┘ └┘ ┴└
st ───┘ └─────────────────────────────────────────────────────
296
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
297 /-- The infimum of insert a s is the minimum of a and the infimum of s, if s is
298 nonempty and bounded below.-/
299 theorem cInf_insert (_ : bdd_below s) (sne : s.nonempty) : Inf (insert a s) = a ⊓ Inf s :=
id └───────┘ ┴ ┴└───────┘ └─┘ └────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
src └───────┘ └───────┘ └─┘ └────┘ ┴ ┴ └─┘
typ └───────┘ ┴ ┴└───────┘ └─┘ └────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
doc └───────┘ └───────┘ └─┘ └─┘
300 calc Inf (insert a s)
id └─┘ └────┘ ┴ ┴
src └─┘ └────┘
typ └─┘ └────┘ ┴ ┴
doc └─┘
301 = Inf ({a} ∪ s) : by rw [insert_eq]
id └─┘ ┴┴ ┴ ┴ └───────┘
src └─┘ ┴ ┴ └──┘└───────┘└─
typ └─┘ ┴┴ ┴ ┴ └──┘└───────┘└─
doc └─┘ └──┘ └─
txt └──┘ └─
par └──┘ └─
pid └┘ ┴└
st └────────────┘┴└
302 ... = Inf {a} ⊓ Inf s : by apply cInf_union _ _ ‹bdd_below s› sne; simp only [ne.def, not_false_iff, set.singleton_nonempty, bdd_below_singleton]
id └─┘ ┴┴ ┴ └─┘ ┴ └────────┘ ┴└───────┘ ┴┴ └─┘ └────┘ └───────────┘ └────────────────────┘ └─────────────────┘
src ───┘ └─┘ ┴ ┴ └─┘ └────┘└────────┘└───┘┴└───────┘┴ ┴┴ └─────────┘└────┘└┘└───────────┘└┘└────────────────────┘└┘└─────────────────┘└─
typ ───┘ └─┘ ┴┴ ┴ └─┘ ┴ └────┘└────────┘└───┘┴└───────┘┴┴┴┴└─┘ └─────────┘└────┘└┘└───────────┘└┘└────────────────────┘└┘└─────────────────┘└─
doc ───┘ └─┘ └─┘ └────┘└────────┘└───┘┴└───────┘┴ ┴┴ └─────────┘ └┘ └┘ └┘ └─
txt ───┘ └────┘ └───┘ ┴ ┴ └─────────┘ └┘ └┘ └┘ └─
par ───┘ └────┘ └───┘ ┴ ┴ └─────────┘ └┘ └┘ └┘ └─
pid ───┘ ┴ └───┘ ┴ ┴ ┴└──┘└┘ └┘ └┘ └┘ ┴└
st ───┘ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
303 ... = a ⊓ Inf s : by simp only [eq_self_iff_true, lattice.cInf_singleton]
id ┴ ┴ └─┘ ┴ └──────────────┘ └────────────────────┘
src ───┘ ┴ └─┘ └─────────┘└──────────────┘└┘└────────────────────┘└─
typ ───┘ ┴ ┴ └─┘ ┴ └─────────┘└──────────────┘└┘└────────────────────┘└─
doc ───┘ └─┘ └─────────┘ └┘└────────────────────┘└─
txt ───┘ └─────────┘ └┘ └─
par ───┘ └─────────┘ └┘ └─
pid ───┘ ┴└──┘└┘ └┘ ┴└
st ───┘ └─────────────────────────────────────────────────────
304
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
305 @[simp] lemma cInf_interval : Inf {b | a ≤ b} = a :=
id └─┘ ┴┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴
typ └─┘ ┴┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └─┘
306 cInf_of_mem_of_le (by simp only [set.mem_set_of_eq]) (λw Hw, by simp only [set.mem_set_of_eq] at Hw; apply Hw)
id └───────────────┘ └───────────────┘ ┴ └┘ └───────────────┘
src └───────────────┘ └─────────┘└───────────────┘┴ └─────────┘└───────────────┘└─────┘ └────┘
typ └───────────────┘ └─────────┘└───────────────┘┴ ┴ └┘ └─────────┘└───────────────┘└─────┘ └────┘
doc └───────────────┘ └─────────┘ ┴ └─────────┘ └─────┘ └────┘
txt └─────────┘ ┴ └─────────┘ └─────┘ └────┘
par └─────────┘ ┴ └─────────┘ └─────┘ └────┘
pid ┴└──┘└┘ ┴ ┴└──┘└┘ ┴┴└───┘ ┴
st └────────────────────────────┘ └────────────────────────────────────────────┘
307
308 @[simp] lemma cSup_interval : Sup {b | b ≤ a} = a :=
id └─┘ ┴┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴
typ └─┘ ┴┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └─┘
309 cSup_of_mem_of_le (by simp only [set.mem_set_of_eq]) (λw Hw, by simp only [set.mem_set_of_eq] at Hw; apply Hw)
id └───────────────┘ └───────────────┘ ┴ └┘ └───────────────┘
src └───────────────┘ └─────────┘└───────────────┘┴ └─────────┘└───────────────┘└─────┘ └────┘
typ └───────────────┘ └─────────┘└───────────────┘┴ ┴ └┘ └─────────┘└───────────────┘└─────┘ └────┘
doc └───────────────┘ └─────────┘ ┴ └─────────┘ └─────┘ └────┘
txt └─────────┘ ┴ └─────────┘ └─────┘ └────┘
par └─────────┘ ┴ └─────────┘ └─────┘ └────┘
pid ┴└──┘└┘ ┴ ┴└──┘└┘ ┴┴└───┘ ┴
st └────────────────────────────┘ └────────────────────────────────────────────┘
310
311 /--The indexed supremum of two functions are comparable if the functions are pointwise comparable-/
312 lemma csupr_le_csupr {f g : ι → α} (B : bdd_above (range g)) (H : ∀x, f x ≤ g x) :
id ┴ ┴ └───────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ └───┘ ┴
typ ┴ ┴ └───────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘ └───┘
313 supr f ≤ supr g :=
id └──┘ ┴ ┴ └──┘ ┴
src └──┘ ┴ └──┘
typ └──┘ ┴ ┴ └──┘ ┴
doc └──┘ └──┘
314 begin
st └─────
315 classical, by_cases hι : nonempty ι,
id └──────┘ ┴
src └───────┘ └───────┘ └─┘└──────┘┴
typ └───────┘ └───────┘ └─┘└──────┘┴┴
doc └───────┘ └───────┘ └─┘ ┴
txt └───────┘ └───────┘ └─┘ ┴
par └───────┘ └───────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ──────────┘└────────────────────────┘└─
316 { have Rf : (range f).nonempty := range_nonempty _,
id └───┘ ┴ └────────────┘
src └────────┘ └───┘┴ └────────────┘└────────────┘└┘
typ └────────┘ └───┘┴┴└────────────┘└────────────┘└┘
doc └────────┘ └───┘┴ └────────────┘ └┘
txt └────────┘ ┴ └────────────┘ └┘
par └────────┘ ┴ └────────────┘ └┘
pid └─────┘└─┘ ┴ └───────┘└───┘ └┘
st ───┘└──────────────────────────────────────────────┘└─
317 apply cSup_le Rf,
id └─────┘ └┘
src └────┘└─────┘┴
typ └────┘└─────┘┴└┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────┘└─
318 rintros y ⟨x, rfl⟩,
src └────────────────┘
typ └────────────────┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid └─────────┘
st ─────────────────────┘└─
319 have : g x ∈ range g := ⟨x, rfl⟩,
id ┴ ┴ └───┘ ┴ ┴ └─┘
src └─────┘ ┴ ┴┴┴└───┘┴ └──┘ └┘└─┘┴
typ └─────┘ ┴┴┴┴┴└───┘┴┴└──┘ ┴└┘└─┘┴
doc └─────┘ ┴ ┴ ┴└───┘┴ └──┘ └┘ ┴
txt └─────┘ ┴ ┴ ┴ ┴ └──┘ └┘ ┴
par └─────┘ ┴ ┴ ┴ ┴ └──┘ └┘ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ └──┘ └┘ ┴
st ───────────────────────────────────┘└─
320 exact le_cSup_of_le B this (H x) },
id └───────────┘ ┴ └──┘ ┴ ┴
src └────┘└───────────┘┴ ┴ ┴ ┴ └┘
typ └────┘└───────────┘┴┴┴└──┘┴ ┴┴┴└┘
doc └────┘ ┴ ┴ ┴ ┴ └┘
txt └────┘ ┴ ┴ ┴ ┴ └┘
par └────┘ ┴ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴ ┴┴
st ────────────────────────────────────┘└┘└
321 { have Rf : range f = ∅, from range_eq_empty.2 hι,
id └───┘ ┴ ┴ ┴ └────────────┘ └┘
src └────────┘└───┘┴ ┴┴┴┴ └───┘└────────────┘└─┘
typ └────────┘└───┘┴┴┴┴┴┴ └───┘└────────────┘└─┘└┘
doc └────────┘└───┘┴ ┴ ┴ └───┘ └─┘
txt └────────┘ ┴ ┴ ┴ └───┘ └─┘
par └────────┘ ┴ ┴ ┴ └───┘ └─┘
pid └─────┘└─┘ ┴ ┴ ┴ └───┘ └─┘
st ────────────────────────┘└────────────────────────┘└─
322 have Rg : range g = ∅, from range_eq_empty.2 hι,
id └───┘ ┴ └────────────┘ └┘
src └────────┘└───┘┴ ┴ ┴ └───┘└────────────┘└─┘
typ └────────┘└───┘┴┴┴ ┴ └───┘└────────────┘└─┘└┘
doc └────────┘└───┘┴ ┴ ┴ └───┘ └─┘
txt └────────┘ ┴ ┴ ┴ └───┘ └─┘
par └────────┘ ┴ ┴ ┴ └───┘ └─┘
pid └─────┘└─┘ ┴ ┴ ┴ └───┘ └─┘
st ────────────────────────┘└────────────────────────┘└─
323 unfold supr, rw [Rf, Rg] }
id └┘ └┘
src └─────────┘ └──┘ └┘ └┘
typ └─────────┘ └──┘└┘└┘└┘└┘
doc └─────────┘ └──┘ └┘ └┘
txt └─────────┘ └──┘ └┘ └┘
par └─────────┘ └──┘ └┘ └┘
pid └───┘ └┘ └┘ ┴┴
st ──────────────┘└──────┘└──┘┴┴└─
324 end
st ──┘
325
326 /--The indexed supremum of a function is bounded above by a uniform bound-/
327 lemma csupr_le [nonempty ι] {f : ι → α} {c : α} (H : ∀x, f x ≤ c) : supr f ≤ c :=
id └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src └──────┘ ┴ └──┘ ┴
typ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘
328 cSup_le (range_nonempty f) (by rwa forall_range_iff)
id └─────┘ └────────────┘ ┴ └──────────────┘
src └─────┘ └────────────┘ └──┘└──────────────┘
typ └─────┘ └────────────┘ ┴ └──┘└──────────────┘
doc └──┘
txt └──┘
par └──┘
pid ┴
st └───────────────────┘
329
330 /--The indexed supremum of a function is bounded below by the value taken at one point-/
331 lemma le_csupr {f : ι → α} (H : bdd_above (range f)) {c : ι} : f c ≤ supr f :=
id ┴ ┴ └───────┘ └───┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
src └───────┘ └───┘ ┴ └──┘
typ ┴ ┴ └───────┘ └───┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
doc └───────┘ └───┘ └──┘
332 le_cSup H (mem_range_self _)
id └─────┘ ┴ └────────────┘
src └─────┘ └────────────┘
typ └─────┘ ┴ └────────────┘
333
334 /--The indexed infimum of two functions are comparable if the functions are pointwise comparable-/
335 lemma cinfi_le_cinfi {f g : ι → α} (B : bdd_below (range f)) (H : ∀x, f x ≤ g x) :
id ┴ ┴ └───────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ └───┘ ┴
typ ┴ ┴ └───────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘ └───┘
336 infi f ≤ infi g :=
id └──┘ ┴ ┴ └──┘ ┴
src └──┘ ┴ └──┘
typ └──┘ ┴ ┴ └──┘ ┴
doc └──┘ └──┘
337 begin
st └─────
338 classical, by_cases hι : nonempty ι,
id └──────┘ ┴
src └───────┘ └───────┘ └─┘└──────┘┴
typ └───────┘ └───────┘ └─┘└──────┘┴┴
doc └───────┘ └───────┘ └─┘ ┴
txt └───────┘ └───────┘ └─┘ ┴
par └───────┘ └───────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ──────────┘└────────────────────────┘└─
339 { have Rg : (range g).nonempty, from range_nonempty _,
id └───┘ ┴ └────────────┘
src └────────┘ └───┘┴ └────────┘ └───┘└────────────┘└┘
typ └────────┘ └───┘┴┴└────────┘ └───┘└────────────┘└┘
doc └────────┘ └───┘┴ └────────┘ └───┘ └┘
txt └────────┘ ┴ └────────┘ └───┘ └┘
par └────────┘ ┴ └────────┘ └───┘ └┘
pid └─────┘└─┘ ┴ └───────┘┴ └───┘ └┘
st ───┘└──────────────────────────┘└─────────────────────┘└─
340 apply le_cInf Rg,
id └─────┘ └┘
src └────┘└─────┘┴
typ └────┘└─────┘┴└┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────┘└─
341 rintros y ⟨x, rfl⟩,
src └────────────────┘
typ └────────────────┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid └─────────┘
st ─────────────────────┘└─
342 have : f x ∈ range f := ⟨x, rfl⟩,
id ┴ ┴ └───┘ ┴ ┴ └─┘
src └─────┘ ┴ ┴┴┴└───┘┴ └──┘ └┘└─┘┴
typ └─────┘ ┴┴┴┴┴└───┘┴┴└──┘ ┴└┘└─┘┴
doc └─────┘ ┴ ┴ ┴└───┘┴ └──┘ └┘ ┴
txt └─────┘ ┴ ┴ ┴ ┴ └──┘ └┘ ┴
par └─────┘ ┴ ┴ ┴ ┴ └──┘ └┘ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ └──┘ └┘ ┴
st ───────────────────────────────────┘└─
343 exact cInf_le_of_le B this (H x) },
id └───────────┘ ┴ └──┘ ┴ ┴
src └────┘└───────────┘┴ ┴ ┴ ┴ └┘
typ └────┘└───────────┘┴┴┴└──┘┴ ┴┴┴└┘
doc └────┘ ┴ ┴ ┴ ┴ └┘
txt └────┘ ┴ ┴ ┴ ┴ └┘
par └────┘ ┴ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴ ┴┴
st ────────────────────────────────────┘└┘└
344 { have Rf : range f = ∅, from range_eq_empty.2 hι,
id └───┘ ┴ ┴ ┴ └────────────┘ └┘
src └────────┘└───┘┴ ┴┴┴┴ └───┘└────────────┘└─┘
typ └────────┘└───┘┴┴┴┴┴┴ └───┘└────────────┘└─┘└┘
doc └────────┘└───┘┴ ┴ ┴ └───┘ └─┘
txt └────────┘ ┴ ┴ ┴ └───┘ └─┘
par └────────┘ ┴ ┴ ┴ └───┘ └─┘
pid └─────┘└─┘ ┴ ┴ ┴ └───┘ └─┘
st ────────────────────────┘└────────────────────────┘└─
345 have Rg : range g = ∅, from range_eq_empty.2 hι,
id └───┘ ┴ └────────────┘ └┘
src └────────┘└───┘┴ ┴ ┴ └───┘└────────────┘└─┘
typ └────────┘└───┘┴┴┴ ┴ └───┘└────────────┘└─┘└┘
doc └────────┘└───┘┴ ┴ ┴ └───┘ └─┘
txt └────────┘ ┴ ┴ ┴ └───┘ └─┘
par └────────┘ ┴ ┴ ┴ └───┘ └─┘
pid └─────┘└─┘ ┴ ┴ ┴ └───┘ └─┘
st ────────────────────────┘└────────────────────────┘└─
346 unfold infi, rw [Rf, Rg] }
id └┘ └┘
src └─────────┘ └──┘ └┘ └┘
typ └─────────┘ └──┘└┘└┘└┘└┘
doc └─────────┘ └──┘ └┘ └┘
txt └─────────┘ └──┘ └┘ └┘
par └─────────┘ └──┘ └┘ └┘
pid └───┘ └┘ └┘ ┴┴
st ──────────────┘└──────┘└──┘┴┴└─
347 end
st ──┘
348
349 /--The indexed minimum of a function is bounded below by a uniform lower bound-/
350 lemma le_cinfi [nonempty ι] {f : ι → α} {c : α} (H : ∀x, c ≤ f x) : c ≤ infi f :=
id └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
src └──────┘ ┴ ┴ └──┘
typ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
doc └──┘
351 le_cInf (range_nonempty f) (by rwa forall_range_iff)
id └─────┘ └────────────┘ ┴ └──────────────┘
src └─────┘ └────────────┘ └──┘└──────────────┘
typ └─────┘ └────────────┘ ┴ └──┘└──────────────┘
doc └──┘
txt └──┘
par └──┘
pid ┴
st └───────────────────┘
352
353 /--The indexed infimum of a function is bounded above by the value taken at one point-/
354 lemma cinfi_le {f : ι → α} (H : bdd_below (range f)) {c : ι} : infi f ≤ f c :=
id ┴ ┴ └───────┘ └───┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
src └───────┘ └───┘ └──┘ ┴
typ ┴ ┴ └───────┘ └───┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
doc └───────┘ └───┘ └──┘
355 cInf_le H (mem_range_self _)
id └─────┘ ┴ └────────────┘
src └─────┘ └────────────┘
typ └─────┘ ┴ └────────────┘
356
357 lemma is_lub_cSup {s : set α} (ne : s.nonempty) (H : bdd_above s) : is_lub s (Sup s) :=
id └─┘ ┴ ┴└───────┘ └───────┘ ┴ └────┘ ┴ └─┘ ┴
src └─┘ └───────┘ └───────┘ └────┘ └─┘
typ └─┘ ┴ ┴└───────┘ └───────┘ ┴ └────┘ ┴ └─┘ ┴
doc └───────┘ └───────┘ └────┘ └─┘
358 ⟨assume x, le_cSup H, assume x, cSup_le ne⟩
id ┴ └─────┘ ┴ ┴ └─────┘ └┘
src └─────┘ └─────┘ └┘
typ ┴ └─────┘ ┴ ┴ └─────┘ └┘
359
360 lemma is_glb_cInf {s : set α} (ne : s.nonempty) (H : bdd_below s) : is_glb s (Inf s) :=
id └─┘ ┴ ┴└───────┘ └───────┘ ┴ └────┘ ┴ └─┘ ┴
src └─┘ └───────┘ └───────┘ └────┘ └─┘
typ └─┘ ┴ ┴└───────┘ └───────┘ ┴ └────┘ ┴ └─┘ ┴
doc └───────┘ └───────┘ └────┘ └─┘
361 ⟨assume x, cInf_le H, assume x, le_cInf ne⟩
id ┴ └─────┘ ┴ ┴ └─────┘ └┘
src └─────┘ └─────┘ └┘
typ ┴ └─────┘ ┴ ┴ └─────┘ └┘
362
363 @[simp] theorem cinfi_const [hι : nonempty ι] {a : α} : (⨅ b:ι, a) = a :=
id └──────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └──────┘ ┴ ┴ ┴
typ └──────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc └──┘ ┴ ┴
364 begin
st └─────
365 refine hι.elim (λ x, _),
id └─────┘
src └─────┘└─────┘┴ └────┘
typ └─────┘└─────┘┴ └────┘
doc └─────┘ ┴ └────┘
txt └─────┘ ┴ └────┘
par └─────┘ ┴ └────┘
pid ┴ ┴ └────┘
st ────────────────────────┘└─
366 refine le_antisymm (@cinfi_le _ _ _ _ _ x) (le_cinfi (λi, _root_.le_refl _)),
id └─────────┘ └──────┘ ┴ └──────┘ └────────────┘
src └─────┘└─────────┘┴ └──────┘└─────────┘ └┘ └──────┘┴ └─┘└────────────┘└──┘
typ └─────┘└─────────┘┴ └──────┘└─────────┘┴└┘ └──────┘┴ └─┘└────────────┘└──┘
doc └─────┘ ┴ └──────┘└─────────┘ └┘ └──────┘┴ └─┘ └──┘
txt └─────┘ ┴ └─────────┘ └┘ ┴ └─┘ └──┘
par └─────┘ ┴ └─────────┘ └┘ ┴ └─┘ └──┘
pid ┴ ┴ └─────────┘ └┘ ┴ └─┘ └──┘
st ─────────────────────────────────────────────────────────────────────────────┘└─
367 rw range_const,
id └─────────┘
src └─┘└─────────┘
typ └─┘└─────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────┘└─
368 exact bdd_below_singleton
id └─────────────────┘
src └────┘└─────────────────┘┴
typ └────┘└─────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────────┘
369 end
st └─┘
370
371 @[simp] theorem csupr_const [hι : nonempty ι] {a : α} : (⨆ b:ι, a) = a :=
id └──────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └──────┘ ┴ ┴ ┴
typ └──────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc └──┘ ┴ ┴
372 begin
st └─────
373 refine hι.elim (λ x, _),
id └─────┘
src └─────┘└─────┘┴ └────┘
typ └─────┘└─────┘┴ └────┘
doc └─────┘ ┴ └────┘
txt └─────┘ ┴ └────┘
par └─────┘ ┴ └────┘
pid ┴ ┴ └────┘
st ────────────────────────┘└─
374 refine le_antisymm (csupr_le (λi, _root_.le_refl _)) (@le_csupr _ _ _ (λ b:ι, a) _ x),
id └─────────┘ └──────┘ └────────────┘ └──────┘ ┴ ┴ ┴
src └─────┘└─────────┘┴ └──────┘┴ └─┘└────────────┘└───┘ └──────┘└─────┘ └─┘ └┘ └──┘ ┴
typ └─────┘└─────────┘┴ └──────┘┴ └─┘└────────────┘└───┘ └──────┘└─────┘ └─┘┴└┘┴└──┘┴┴
doc └─────┘ ┴ └──────┘┴ └─┘ └───┘ └──────┘└─────┘ └─┘ └┘ └──┘ ┴
txt └─────┘ ┴ ┴ └─┘ └───┘ └─────┘ └─┘ └┘ └──┘ ┴
par └─────┘ ┴ ┴ └─┘ └───┘ └─────┘ └─┘ └┘ └──┘ ┴
pid ┴ ┴ ┴ └─┘ └───┘ └─────┘ └─┘ └┘ └──┘ ┴
st ──────────────────────────────────────────────────────────────────────────────────────┘└─
375 rw range_const,
id └─────────┘
src └─┘└─────────┘
typ └─┘└─────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────┘└─
376 exact bdd_above_singleton
id └─────────────────┘
src └────┘└─────────────────┘┴
typ └────┘└─────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────────┘
377 end
st └─┘
378
379 end conditionally_complete_lattice
380
381
382 section conditionally_complete_linear_order
383 variables [conditionally_complete_linear_order α] {s t : set α} {a b : α}
id └─────────────────────────────────┘ └─┘
src └─────────────────────────────────┘ └─┘
typ └─────────────────────────────────┘ └─┘
384
385 /-- When b < Sup s, there is an element a in s with b < a, if s is nonempty and the order is
386 a linear order. -/
387 lemma exists_lt_of_lt_cSup (hs : s.nonempty) (hb : b < Sup s) : ∃a∈s, b < a :=
id ┴└───────┘ ┴ ┴ └─┘ ┴ ┴┴ ┴┴ ┴ ┴ ┴
src └───────┘ ┴ └─┘ ┴ ┴ ┴
typ ┴└───────┘ ┴ ┴ └─┘ ┴ ┴┴ ┴┴ ┴ ┴ ┴
doc └───────┘ └─┘
388 begin
st └─────
389 classical, contrapose! hb,
src └───────┘ └────────────┘
typ └───────┘ └────────────┘
doc └───────┘ └────────────┘
txt └───────┘ └────────────┘
par └───────┘ └────────────┘
pid ┴└─┘
st ──────────┘└──────────────┘└─
390 exact cSup_le hs hb
id └─────┘ └┘ └┘
src └────┘└─────┘┴ ┴ ┴
typ └────┘└─────┘┴└┘┴└┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ─────────────────────┘
391 end
st └─┘
392
393 /--
394 Indexed version of the above lemma `exists_lt_of_lt_cSup`.
395 When `b < supr f`, there is an element `i` such that `b < f i`.
396 -/
397 lemma exists_lt_of_lt_csupr [nonempty ι] {f : ι → α} (h : b < supr f) :
id └──────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
src └──────┘ ┴ └──┘
typ └──────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
doc └──┘
398 ∃i, b < f i :=
id ┴┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴┴┴ ┴ ┴ ┴ ┴
399 let ⟨_, ⟨i, rfl⟩, h⟩ := exists_lt_of_lt_cSup (range_nonempty f) h in ⟨i, h⟩
id └─┘ ┴ └─┘ ┴ └──────────────────┘ └────────────┘ ┴ ┴
src └─┘ └──────────────────┘ └────────────┘
typ └─┘ ┴ └─┘ ┴ └──────────────────┘ └────────────┘ ┴ ┴
doc └──────────────────┘
400
401 /--When Inf s < b, there is an element a in s with a < b, if s is nonempty and the order is
402 a linear order.-/
403 lemma exists_lt_of_cInf_lt (hs : s.nonempty) (hb : Inf s < b) : ∃a∈s, a < b :=
id ┴└───────┘ └─┘ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
src └───────┘ └─┘ ┴ ┴ ┴ ┴
typ ┴└───────┘ └─┘ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
doc └───────┘ └─┘
404 begin
st └─────
405 classical, contrapose! hb,
src └───────┘ └────────────┘
typ └───────┘ └────────────┘
doc └───────┘ └────────────┘
txt └───────┘ └────────────┘
par └───────┘ └────────────┘
pid ┴└─┘
st ──────────┘└──────────────┘└─
406 exact le_cInf hs hb
id └─────┘ └┘ └┘
src └────┘└─────┘┴ ┴ ┴
typ └────┘└─────┘┴└┘┴└┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ─────────────────────┘
407 end
st └─┘
408
409 /--
410 Indexed version of the above lemma `exists_lt_of_cInf_lt`
411 When `infi f < a`, there is an element `i` such that `f i < a`.
412 -/
413 lemma exists_lt_of_cinfi_lt [nonempty ι] {f : ι → α} (h : infi f < a) :
id └──────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src └──────┘ └──┘ ┴
typ └──────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘
414 (∃i, f i < a) :=
id ┴┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴┴┴ ┴ ┴ ┴ ┴
415 let ⟨_, ⟨i, rfl⟩, h⟩ := exists_lt_of_cInf_lt (range_nonempty f) h in ⟨i, h⟩
id └─┘ ┴ └─┘ ┴ └──────────────────┘ └────────────┘ ┴ ┴
src └─┘ └──────────────────┘ └────────────┘
typ └─┘ ┴ └─┘ ┴ └──────────────────┘ └────────────┘ ┴ ┴
doc └──────────────────┘
416
417 /--Introduction rule to prove that b is the supremum of s: it suffices to check that
418 1) b is an upper bound
419 2) every other upper bound b' satisfies b ≤ b'.-/
420 theorem cSup_intro' (_ : s.nonempty)
id ┴└───────┘
src └───────┘
typ ┴└───────┘
doc └───────┘
421 (h_is_ub : ∀ a ∈ s, a ≤ b) (h_b_le_ub : ∀ub, (∀ a ∈ s, a ≤ ub) → (b ≤ ub)) : Sup s = b :=
id ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └─┘ ┴ ┴ ┴
src ┴ ┴ ┴ └─┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └─┘ ┴ ┴ ┴
doc └─┘
422 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
423 (show Sup s ≤ b, from cSup_le ‹s.nonempty› h_is_ub)
id └─┘ ┴ ┴ ┴ └─────┘ ┴┴└───────┘┴ └─────┘
src └─┘ ┴ └─────┘ ┴ └───────┘┴
typ └─┘ ┴ ┴ ┴ └─────┘ ┴┴└───────┘┴ └─────┘
doc └─┘ ┴ └───────┘┴
424 (show b ≤ Sup s, from h_b_le_ub _ $ assume a, le_cSup ⟨b, h_is_ub⟩)
id ┴ ┴ └─┘ ┴ └───────┘ ┴ └─────┘ ┴ └─────┘
src ┴ └─┘ └─────┘
typ ┴ ┴ └─┘ ┴ └───────┘ ┴ └─────┘ ┴ └─────┘
doc └─┘
425
426 end conditionally_complete_linear_order
427
428 section conditionally_complete_linear_order_bot
429
430 lemma cSup_empty [conditionally_complete_linear_order_bot α] : (Sup ∅ : α) = ⊥ :=
id └─────────────────────────────────────┘ ┴ └─┘ ┴ ┴ ┴ ┴
src └─────────────────────────────────────┘ └─┘ ┴ ┴ ┴
typ └─────────────────────────────────────┘ ┴ └─┘ ┴ ┴ ┴ ┴
doc └─┘
431 conditionally_complete_linear_order_bot.cSup_empty α
id └────────────────────────────────────────────────┘ ┴
src └────────────────────────────────────────────────┘
typ └────────────────────────────────────────────────┘ ┴
432
433 end conditionally_complete_linear_order_bot
434
435 section
436
437 open_locale classical
438
439 noncomputable instance : has_Inf ℕ :=
id └─────┘ ┴
src └─────┘ ┴
typ └─────┘ ┴
doc └─────┘
440 ⟨λs, if h : ∃n, n ∈ s then @nat.find (λn, n ∈ s) _ h else 0⟩
id ┴ └┘ ┴┴┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ ┴ ┴ └──────┘ ┴ ┴
typ ┴ └┘ ┴┴┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
441
442 noncomputable instance : has_Sup ℕ :=
id └─────┘ ┴
src └─────┘ ┴
typ └─────┘ ┴
doc └─────┘
443 ⟨λs, if h : ∃n, ∀a∈s, a ≤ n then @nat.find (λn, ∀a∈s, a ≤ n) _ h else 0⟩
id ┴ └┘ ┴┴┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ ┴ ┴ └──────┘ ┴
typ ┴ └┘ ┴┴┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
444
445 lemma Inf_nat_def {s : set ℕ} (h : ∃n, n ∈ s) : Inf s = @nat.find (λn, n ∈ s) _ h :=
id └─┘ ┴ ┴┴┴ ┴ ┴ ┴ └─┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ └──────┘ ┴
typ └─┘ ┴ ┴┴┴ ┴ ┴ ┴ └─┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
doc └─┘
446 dif_pos _
id └─────┘
src └─────┘
typ └─────┘
447
448 lemma Sup_nat_def {s : set ℕ} (h : ∃n, ∀a∈s, a ≤ n) :
id └─┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴
449 Sup s = @nat.find (λn, ∀a∈s, a ≤ n) _ h :=
id └─┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ └──────┘ ┴
typ └─┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
450 dif_pos _
id └─────┘
src └─────┘
typ └─────┘
451
452 /-- This instance is necessary, otherwise the lattice operations would be derived via
453 conditionally_complete_linear_order_bot and marked as noncomputable. -/
454 instance : lattice ℕ := infer_instance
id └─────┘ ┴ └────────────┘
src └─────┘ ┴ └────────────┘
typ └─────┘ ┴ └────────────┘
doc └─────┘ └────────────┘
455
456 noncomputable instance : conditionally_complete_linear_order_bot ℕ :=
id └─────────────────────────────────────┘ ┴
src └─────────────────────────────────────┘ ┴
typ └─────────────────────────────────────┘ ┴
457 { Sup := Sup, Inf := Inf,
id └─┘ └─┘
src └─┘ └─┘
typ └─┘ └─┘
doc └─┘ └─┘
458 le_cSup := assume s a hb ha, by rw [Sup_nat_def hb]; revert a ha; exact @nat.find_spec _ _ hb,
id ┴ ┴ └┘ └┘ └─────────┘ └┘ └───────────┘ └┘
src └──┘└─────────┘┴ ┴ └─────────┘ └────┘ └───────────┘└───┘
typ ┴ ┴ └┘ └┘ └──┘└─────────┘┴└┘┴ └─────────┘ └────┘ └───────────┘└───┘└┘
doc └──┘ ┴ ┴ └─────────┘ └────┘ └───┘
txt └──┘ ┴ ┴ └─────────┘ └────┘ └───┘
par └──┘ ┴ ┴ └─────────┘ └────┘ └───┘
pid └┘ ┴ ┴ └───┘ ┴ └───┘
st └─────────────────┘┴└────────────────────────────────────────┘
459 cSup_le := assume s a hs ha, by rw [Sup_nat_def ⟨a, ha⟩]; exact nat.find_min' _ ha,
id ┴ ┴ └┘ └┘ └─────────┘ ┴ └┘ └───────────┘ └┘
src └──┘└─────────┘┴ └┘ └┘ └────┘└───────────┘└─┘
typ ┴ ┴ └┘ └┘ └──┘└─────────┘┴ ┴└┘└┘└┘ └────┘└───────────┘└─┘└┘
doc └──┘ ┴ └┘ └┘ └────┘ └─┘
txt └──┘ ┴ └┘ └┘ └────┘ └─┘
par └──┘ ┴ └┘ └┘ └────┘ └─┘
pid └┘ ┴ └┘ └┘ ┴ └─┘
st └──────────────────────┘┴└────────────────────────┘
460 le_cInf := assume s a hs hb,
id ┴ ┴ └┘ └┘
typ ┴ ┴ └┘ └┘
461 by rw [Inf_nat_def hs]; exact hb (@nat.find_spec (λn, n ∈ s) _ _),
id └─────────┘ └┘ └┘ └───────────┘ ┴ ┴
src └──┘└─────────┘┴ ┴ └────┘ ┴ └───────────┘┴ └─┘ ┴┴┴ └────┘
typ └──┘└─────────┘┴└┘┴ └────┘└┘┴ └───────────┘┴ └─┘ ┴┴┴┴└────┘
doc └──┘ ┴ ┴ └────┘ ┴ ┴ └─┘ ┴ ┴ └────┘
txt └──┘ ┴ ┴ └────┘ ┴ ┴ └─┘ ┴ ┴ └────┘
par └──┘ ┴ ┴ └────┘ ┴ ┴ └─┘ ┴ ┴ └────┘
pid └┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └────┘
st └─────────────────┘┴└─────────────────────────────────────────┘
462 cInf_le := assume s a hb ha, by rw [Inf_nat_def ⟨a, ha⟩]; exact nat.find_min' _ ha,
id ┴ ┴ └┘ └┘ └─────────┘ ┴ └┘ └───────────┘ └┘
src └──┘└─────────┘┴ └┘ └┘ └────┘└───────────┘└─┘
typ ┴ ┴ └┘ └┘ └──┘└─────────┘┴ ┴└┘└┘└┘ └────┘└───────────┘└─┘└┘
doc └──┘ ┴ └┘ └┘ └────┘ └─┘
txt └──┘ ┴ └┘ └┘ └────┘ └─┘
par └──┘ ┴ └┘ └┘ └────┘ └─┘
pid └┘ ┴ └┘ └┘ ┴ └─┘
st └──────────────────────┘┴└────────────────────────┘
463 cSup_empty :=
464 begin
st └─────
465 simp only [Sup_nat_def, set.mem_empty_eq, forall_const, forall_prop_of_false, not_false_iff, exists_const],
id └─────────┘ └──────────────┘ └──────────┘ └──────────────────┘ └───────────┘ └──────────┘
src └─────────┘└─────────┘└┘└──────────────┘└┘└──────────┘└┘└──────────────────┘└┘└───────────┘└┘└──────────┘┴
typ └─────────┘└─────────┘└┘└──────────────┘└┘└──────────┘└┘└──────────────────┘└┘└───────────┘└┘└──────────┘┴
doc └─────────┘ └┘ └┘ └┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ └┘ ┴
st ─────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
466 apply bot_unique (nat.find_min' _ _),
id └────────┘ └───────────┘
src └────┘└────────┘┴ └───────────┘└───┘
typ └────┘└────────┘┴ └───────────┘└───┘
doc └────┘ ┴ └───┘
txt └────┘ ┴ └───┘
par └────┘ ┴ └───┘
pid ┴ ┴ └───┘
st ───────────────────────────────────────┘└─
467 trivial
src └───────
typ └───────
doc └───────
txt └───────
par └───────
pid └
st ────────────
468 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
469 .. (infer_instance : order_bot ℕ), .. (infer_instance : lattice ℕ),
id └────────────┘ └───────┘ ┴ └────────────┘ └─────┘ ┴
src └────────────┘ └───────┘ ┴ └────────────┘ └─────┘ ┴
typ └────────────┘ └───────┘ ┴ └────────────┘ └─────┘ ┴
doc └────────────┘ └───────┘ └────────────┘ └─────┘
470 .. (infer_instance : decidable_linear_order ℕ) }
id └────────────┘ └────────────────────┘ ┴
src └────────────┘ └────────────────────┘ ┴
typ └────────────┘ └────────────────────┘ ┴
doc └────────────┘
471
472 end
473
474 end lattice /-end of namespace lattice-/
475
476 namespace with_top
477 open lattice
478 open_locale classical
479
480 variables [conditionally_complete_linear_order_bot α]
id └─────────────────────────────────────┘
src └─────────────────────────────────────┘
typ └─────────────────────────────────────┘
481
482 /-- The Sup of a non-empty set is its least upper bound for a conditionally
483 complete lattice with a top. -/
484 lemma is_lub_Sup' {β : Type*} [conditionally_complete_lattice β]
id └────────────────────────────┘ ┴
src └────────────────────────────┘
typ └────────────────────────────┘ ┴
doc └────────────────────────────┘
485 {s : set (with_top β)} (hs : s.nonempty) : is_lub s (Sup s) :=
id └─┘ └──────┘ ┴ ┴└───────┘ └────┘ ┴ └─┘ ┴
src └─┘ └──────┘ └───────┘ └────┘ └─┘
typ └─┘ └──────┘ ┴ ┴└───────┘ └────┘ ┴ └─┘ ┴
doc └───────┘ └────┘ └─┘
486 begin
st └─────
487 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
488 { show ite _ _ _ ∈ _,
id └─┘ ┴
src └───┘└─┘└─────┘┴└┘
typ └───┘└─┘└─────┘┴└┘
doc └───┘ └─────┘ └┘
txt └───┘ └─────┘ └┘
par └───┘ └─────┘ └┘
pid └───┘ └─────┘ └┘
st ───┘└────────────────┘└─
489 split_ifs,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
st ────────────┘└─
490 { intros _ _, exact le_top },
id └────┘
src └────────┘ └────┘└────┘┴
typ └────────┘ └────┘└────┘┴
doc └────────┘ └────┘ ┴
txt └────────┘ └────┘ ┴
par └────────┘ └────┘ ┴
pid └──┘ ┴ ┴
st ─────┘└────────┘└─────────────┘└┘└
491 { rintro (⟨⟩|a) ha,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └────────┘
st ─────┘└──────────────┘└─
492 { contradiction },
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴
st ───────┘└────────────┘└┘└
493 apply some_le_some.2,
id └──────────┘
src └────┘└──────────┘└┘
typ └────┘└──────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ └┘
st ─────────────────────────┘└─
494 exact le_cSup h_1 ha },
id └─────┘ └─┘ └┘
src └────┘└─────┘┴ ┴ ┴
typ └────┘└─────┘┴└─┘┴└┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ──────────────────────────┘└┘└
495 { intros _ _, exact le_top } },
id └────┘
src └────────┘ └────┘└────┘┴
typ └────────┘ └────┘└────┘┴
doc └────────┘ └────┘ ┴
txt └────────┘ └────┘ ┴
par └────────┘ └────┘ ┴
pid └──┘ ┴ ┴
st ───────────────┘└─────────────┘└──┘└
496 { show ite _ _ _ ∈ _,
id └─┘
src └───┘└─┘└─────┘ └┘
typ └───┘└─┘└─────┘ └┘
doc └───┘ └─────┘ └┘
txt └───┘ └─────┘ └┘
par └───┘ └─────┘ └┘
pid └───┘ └─────┘ └┘
st ─────────────────────┘└─
497 split_ifs,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
st ────────────┘└─
498 { rintro (⟨⟩|a) ha,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └────────┘
st ─────┘└──────────────┘└─
499 { exact _root_.le_refl _ },
id └────────────┘
src └────┘└────────────┘└─┘
typ └────┘└────────────┘└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └┘┴
st ───────┘└─────────────────────┘└┘└
500 { exact false.elim (not_top_le_coe a (ha h)) } },
id └────────┘ └────────────┘ ┴ └┘ ┴
src └────┘└────────┘┴ └────────────┘┴ ┴ ┴ └─┘
typ └────┘└────────┘┴ └────────────┘┴┴┴ └┘┴┴└─┘
doc └────┘ ┴ ┴ ┴ ┴ └─┘
txt └────┘ ┴ ┴ ┴ ┴ └─┘
par └────┘ ┴ ┴ ┴ ┴ └─┘
pid ┴ ┴ ┴ ┴ ┴ └┘┴
st ──────────────────────────────────────────────────┘└──┘└
501 { rintro (⟨⟩|b) hb,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └────────┘
st ─────┘└──────────────┘└─
502 { exact le_top },
id └────┘
src └────┘└────┘┴
typ └────┘└────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────┘└───────────┘└┘└
503 refine some_le_some.2 (cSup_le _ _),
id └──────────┘ └─────┘
src └─────┘└──────────┘└─┘ └─────┘└───┘
typ └─────┘└──────────┘└─┘ └─────┘└───┘
doc └─────┘ └─┘ └───┘
txt └─────┘ └─┘ └───┘
par └─────┘ └─┘ └───┘
pid ┴ └─┘ └───┘
st ────────────────────────────────────────┘└─
504 { rcases hs with ⟨⟨⟩|b, hb⟩,
id └┘
src └─────┘ └──────────────┘
typ └─────┘└┘└──────────────┘
doc └─────┘ └──────────────┘
txt └─────┘ └──────────────┘
par └─────┘ └──────────────┘
pid ┴ └──────────────┘
st ───────┘└───────────────────────┘└─
505 { exact absurd hb h },
id └────┘ └┘ ┴
src └────┘└────┘┴ ┴ ┴
typ └────┘└────┘┴└┘┴┴┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ─────────┘└────────────────┘└┘└
506 { exact ⟨b, hb⟩ } },
id ┴ └┘
src └────┘ └┘ └┘
typ └────┘ ┴└┘└┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴ └┘ ┴┴
st ───────────────────────┘└──┘└
507 { intros a ha, exact some_le_some.1 (hb ha) } },
id └──────────┘ └┘ └┘
src └─────────┘ └────┘└──────────┘└─┘ ┴ └┘
typ └─────────┘ └────┘└──────────┘└─┘ └┘┴└┘└┘
doc └─────────┘ └────┘ └─┘ ┴ └┘
txt └─────────┘ └────┘ └─┘ ┴ └┘
par └─────────┘ └────┘ └─┘ ┴ └┘
pid └───┘ ┴ └─┘ ┴ ┴┴
st ──────────────────┘└─────────────────────────────┘└──┘└
508 { rintro (⟨⟩|b) hb,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └────────┘
st ─────────────────────┘└─
509 { exact _root_.le_refl _ },
id └────────────┘
src └────┘└────────────┘└─┘
typ └────┘└────────────┘└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └┘┴
st ───────┘└─────────────────────┘└┘└
510 { exfalso, apply h_1, use b, intros a ha, exact some_le_some.1 (hb ha) } } }
id ┴ └──────────┘ └┘ └┘
src └─────┘ └────┘ └──┘ └─────────┘ └────┘└──────────┘└─┘ ┴ └┘
typ └─────┘ └────┘ └──┘┴ └─────────┘ └────┘└──────────┘└─┘ └┘┴└┘└┘
doc └─────┘ └────┘ └──┘ └─────────┘ └────┘ └─┘ ┴ └┘
txt └─────┘ └────┘ └──┘ └─────────┘ └────┘ └─┘ ┴ └┘
par └─────┘ └────┘ └──┘ └─────────┘ └────┘ └─┘ ┴ └┘
pid ┴ ┴ └───┘ ┴ └─┘ ┴ ┴┴
st ──────────────┘└─────────┘└─────┘└───────────┘└─────────────────────────────┘└─────
511 end
st ──┘
512
513 lemma is_lub_Sup (s : set (with_top α)) : is_lub s (Sup s) :=
id └─┘ └──────┘ ┴ └────┘ ┴ └─┘ ┴
src └─┘ └──────┘ └────┘ └─┘
typ └─┘ └──────┘ ┴ └────┘ ┴ └─┘ ┴
doc └────┘ └─┘
514 begin
st └─────
515 cases s.eq_empty_or_nonempty with hs hs,
id └────────────────────┘
src └────┘└────────────────────┘└─────────┘
typ └────┘└────────────────────┘└─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid ┴ └─────────┘
st ────────────────────────────────────────┘└─
516 { rw hs,
id └┘
src └─┘
typ └─┘└┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───┘└───┘└─
517 show is_lub ∅ (ite _ _ _),
id └────┘ ┴ └─┘
src └───┘└────┘┴┴┴ └─┘└─────┘
typ └───┘└────┘┴┴┴ └─┘└─────┘
doc └───┘└────┘┴ ┴ └─────┘
txt └───┘ ┴ ┴ └─────┘
par └───┘ ┴ ┴ └─────┘
pid └───┘ ┴ ┴ └─────┘
st ────────────────────────────┘└─
518 split_ifs,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
st ────────────┘└─
519 { cases h },
id ┴
src └────┘ ┴
typ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────┘└──────┘└┘└
520 { rw [preimage_empty, cSup_empty], exact is_lub_empty },
id └────────────┘ └────────┘ └──────────┘
src └──┘└────────────┘└┘└────────┘┴ └────┘└──────────┘┴
typ └──┘└────────────┘└┘└────────┘┴ └────┘└──────────┘┴
doc └──┘ └┘ ┴ └────┘ ┴
txt └──┘ └┘ ┴ └────┘ ┴
par └──┘ └┘ ┴ └────┘ ┴
pid └┘ └┘ ┴ ┴ ┴
st ─────┘└────────────────┘└──────────┘└────────────────────┘└┘└
521 { exfalso, apply h_1, use ⊥, rintro a ⟨⟩ } },
id ┴
src └─────┘ └────┘ └──┘┴ └──────────┘
typ └─────┘ └────┘ └──┘┴ └──────────┘
doc └─────┘ └────┘ └──┘ └──────────┘
txt └─────┘ └────┘ └──┘ └──────────┘
par └─────┘ └────┘ └──┘ └──────────┘
pid ┴ ┴ └───┘┴
st ────────────┘└─────────┘└─────┘└────────────┘└──┘└
522 exact is_lub_Sup' hs,
id └─────────┘ └┘
src └────┘└─────────┘┴
typ └────┘└─────────┘┴└┘
doc └────┘└─────────┘┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────────┘└─
523 end
st ──┘
524
525 /-- The Inf of a bounded-below set is its greatest lower bound for a conditionally
526 complete lattice with a top. -/
527 lemma is_glb_Inf' {β : Type*} [conditionally_complete_lattice β]
id └────────────────────────────┘ ┴
src └────────────────────────────┘
typ └────────────────────────────┘ ┴
doc └────────────────────────────┘
528 {s : set (with_top β)} (hs : bdd_below s) : is_glb s (Inf s) :=
id └─┘ └──────┘ ┴ └───────┘ ┴ └────┘ ┴ └─┘ ┴
src └─┘ └──────┘ └───────┘ └────┘ └─┘
typ └─┘ └──────┘ ┴ └───────┘ ┴ └────┘ ┴ └─┘ ┴
doc └───────┘ └────┘ └─┘
529 begin
st └─────
530 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
531 { show ite _ _ _ ∈ _,
id └─┘ ┴
src └───┘└─┘└─────┘┴└┘
typ └───┘└─┘└─────┘┴└┘
doc └───┘ └─────┘ └┘
txt └───┘ └─────┘ └┘
par └───┘ └─────┘ └┘
pid └───┘ └─────┘ └┘
st ───┘└────────────────┘└─
532 split_ifs,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
st ────────────┘└─
533 { intros a ha, exact top_le_iff.2 (set.mem_singleton_iff.1 (h ha)) },
id └────────┘ └───────────────────┘ ┴ └┘
src └─────────┘ └────┘└────────┘└─┘ └───────────────────┘└─┘ ┴ └─┘
typ └─────────┘ └────┘└────────┘└─┘ └───────────────────┘└─┘ ┴┴└┘└─┘
doc └─────────┘ └────┘ └─┘ └─┘ ┴ └─┘
txt └─────────┘ └────┘ └─┘ └─┘ ┴ └─┘
par └─────────┘ └────┘ └─┘ └─┘ ┴ └─┘
pid └───┘ ┴ └─┘ └─┘ ┴ └┘┴
st ─────┘└─────────┘└────────────────────────────────────────────────────┘└┘└
534 { rintro (⟨⟩|a) ha,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └────────┘
st ─────────────────────┘└─
535 { exact le_top },
id └────┘
src └────┘└────┘┴
typ └────┘└────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────┘└───────────┘└┘└
536 refine some_le_some.2 (cInf_le _ ha),
id └──────────┘ └─────┘ └┘
src └─────┘└──────────┘└─┘ └─────┘└─┘ ┴
typ └─────┘└──────────┘└─┘ └─────┘└─┘└┘┴
doc └─────┘ └─┘ └─┘ ┴
txt └─────┘ └─┘ └─┘ ┴
par └─────┘ └─┘ └─┘ ┴
pid ┴ └─┘ └─┘ ┴
st ─────────────────────────────────────────┘└─
537 rcases hs with ⟨⟨⟩|b, hb⟩,
id └┘
src └─────┘ └──────────────┘
typ └─────┘└┘└──────────────┘
doc └─────┘ └──────────────┘
txt └─────┘ └──────────────┘
par └─────┘ └──────────────┘
pid ┴ └──────────────┘
st ──────────────────────────────┘└─
538 { exfalso,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
st ───────┘└─────┘└─
539 apply h,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────┘└─
540 intros c hc,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ──────────────────┘└─
541 rw [mem_singleton_iff, ←top_le_iff],
id └───────────────┘ └────────┘
src └──┘└───────────────┘└─┘└────────┘┴
typ └──┘└───────────────┘└─┘└────────┘┴
doc └──┘ └─┘ ┴
txt └──┘ └─┘ ┴
par └──┘ └─┘ ┴
pid └┘ └─┘ ┴
st ────────────────────────────┘└───────────┘└──
542 exact hb hc },
id └┘ └┘
src └────┘ ┴ ┴
typ └────┘└┘┴└┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ───────────────────┘└┘└
543 use b,
id ┴
src └──┘
typ └──┘┴
doc └──┘
txt └──┘
par └──┘
pid ┴
st ──────────┘└─
544 intros c hc,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ────────────────┘└─
545 exact some_le_some.1 (hb hc) } },
id └──────────┘ └┘ └┘
src └────┘└──────────┘└─┘ ┴ └┘
typ └────┘└──────────┘└─┘ └┘┴└┘└┘
doc └────┘ └─┘ ┴ └┘
txt └────┘ └─┘ ┴ └┘
par └────┘ └─┘ ┴ └┘
pid ┴ └─┘ ┴ ┴┴
st ──────────────────────────────────┘└──┘└
546 { show ite _ _ _ ∈ _,
id └─┘
src └───┘└─┘└─────┘ └┘
typ └───┘└─┘└─────┘ └┘
doc └───┘ └─────┘ └┘
txt └───┘ └─────┘ └┘
par └───┘ └─────┘ └┘
pid └───┘ └─────┘ └┘
st ─────────────────────┘└─
547 split_ifs,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
st ────────────┘└─
548 { intros _ _, exact le_top },
id └────┘
src └────────┘ └────┘└────┘┴
typ └────────┘ └────┘└────┘┴
doc └────────┘ └────┘ ┴
txt └────────┘ └────┘ ┴
par └────────┘ └────┘ ┴
pid └──┘ ┴ ┴
st ─────┘└────────┘└─────────────┘└┘└
549 { rintro (⟨⟩|a) ha,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └────────┘
st ─────────────────────┘└─
550 { exfalso, apply h, intros b hb, exact set.mem_singleton_iff.2 (top_le_iff.1 (ha hb)) },
id └───────────────────┘ └────────┘ └┘ └┘
src └─────┘ └────┘ └─────────┘ └────┘└───────────────────┘└─┘ └────────┘└─┘ ┴ └─┘
typ └─────┘ └────┘ └─────────┘ └────┘└───────────────────┘└─┘ └────────┘└─┘ └┘┴└┘└─┘
doc └─────┘ └────┘ └─────────┘ └────┘ └─┘ └─┘ ┴ └─┘
txt └─────┘ └────┘ └─────────┘ └────┘ └─┘ └─┘ ┴ └─┘
par └─────┘ └────┘ └─────────┘ └────┘ └─┘ └─┘ ┴ └─┘
pid ┴ └───┘ ┴ └─┘ └─┘ ┴ └┘┴
st ───────┘└─────┘└───────┘└───────────┘└─────────────────────────────────────────────────────┘└┘└
551 { refine some_le_some.2 (le_cInf _ _),
id └──────────┘ └─────┘
src └─────┘└──────────┘└─┘ └─────┘└───┘
typ └─────┘└──────────┘└─┘ └─────┘└───┘
doc └─────┘ └─┘ └───┘
txt └─────┘ └─┘ └───┘
par └─────┘ └─┘ └───┘
pid ┴ └─┘ └───┘
st ──────────────────────────────────────────┘└─
552 { classical, contrapose! h,
src └───────┘ └───────────┘
typ └───────┘ └───────────┘
doc └───────┘ └───────────┘
txt └───────┘ └───────────┘
par └───────┘ └───────────┘
pid ┴└┘
st ─────────┘└───────┘└─────────────┘└─
553 rintros (⟨⟩|a) ha,
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
txt └───────────────┘
par └───────────────┘
pid └────────┘
st ──────────────────────────┘└─
554 { exact mem_singleton ⊤ },
id └───────────┘ ┴
src └────┘└───────────┘┴┴┴
typ └────┘└───────────┘┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ───────────┘└────────────────────┘└┘└
555 { exact (h ⟨a, ha⟩).elim }},
id ┴ ┴ └┘
src └────┘ ┴ └┘ └──────┘
typ └────┘ ┴┴ ┴└┘└┘└──────┘
doc └────┘ ┴ └┘ └──────┘
txt └────┘ ┴ └┘ └──────┘
par └────┘ ┴ └┘ └──────┘
pid ┴ ┴ └┘ └────┘└┘
st ──────────────────────────────────┘└─┘└
556 { intros b hb,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ────────────────────┘└─
557 rw ←some_le_some,
id └──────────┘
src └──┘└──────────┘
typ └──┘└──────────┘
doc └──┘
txt └──┘
par └──┘
pid └┘
st ─────────────────────────┘└─
558 exact ha hb } } } }
id └┘ └┘
src └────┘ ┴ ┴
typ └────┘└┘┴└┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────────────────────┘└───────
559 end
st ──┘
560
561 lemma is_glb_Inf (s : set (with_top α)) : is_glb s (Inf s) :=
id └─┘ └──────┘ ┴ └────┘ ┴ └─┘ ┴
src └─┘ └──────┘ └────┘ └─┘
typ └─┘ └──────┘ ┴ └────┘ ┴ └─┘ ┴
doc └────┘ └─┘
562 begin
st └─────
563 by_cases hs : bdd_below s,
id └───────┘ ┴
src └───────┘ └─┘└───────┘┴
typ └───────┘ └─┘└───────┘┴┴
doc └───────┘ └─┘└───────┘┴
txt └───────┘ └─┘ ┴
par └───────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ──────────────────────────┘└─
564 { exact is_glb_Inf' hs },
id └─────────┘ └┘
src └────┘└─────────┘┴ ┴
typ └────┘└─────────┘┴└┘┴
doc └────┘└─────────┘┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ───┘└───────────────────┘└┘└
565 { exfalso, apply hs, use ⊥, intros _ _, exact bot_le },
id ┴ └────┘
src └─────┘ └────┘ └──┘┴ └────────┘ └────┘└────┘┴
typ └─────┘ └────┘ └──┘┴ └────────┘ └────┘└────┘┴
doc └─────┘ └────┘ └──┘ └────────┘ └────┘ ┴
txt └─────┘ └────┘ └──┘ └────────┘ └────┘ ┴
par └─────┘ └────┘ └──┘ └────────┘ └────┘ ┴
pid ┴ ┴ └──┘ ┴ ┴
st ──────────┘└────────┘└─────┘└──────────┘└─────────────┘└──
566 end
st ──┘
567
568 noncomputable instance : complete_linear_order (with_top α) :=
id └───────────────────┘ └──────┘ ┴
src └───────────────────┘ └──────┘
typ └───────────────────┘ └──────┘ ┴
doc └───────────────────┘
569 { Sup := Sup, le_Sup := assume s, (is_lub_Sup s).1, Sup_le := assume s, (is_lub_Sup s).2,
id └─┘ ┴ └────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴
src └─┘ └────────┘ ┴ └────────┘ ┴
typ └─┘ ┴ └────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴
doc └─┘
570 Inf := Inf, le_Inf := assume s, (is_glb_Inf s).2, Inf_le := assume s, (is_glb_Inf s).1,
id └─┘ ┴ └────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴
src └─┘ └────────┘ ┴ └────────┘ ┴
typ └─┘ ┴ └────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴
doc └─┘
571 decidable_le := classical.dec_rel _,
id └───────────────┘
src └───────────────┘
typ └───────────────┘
572 .. with_top.linear_order, ..with_top.lattice, ..with_top.order_top, ..with_top.order_bot }
id └───────────────────┘ └──────────────┘ └────────────────┘ └────────────────┘
src └───────────────────┘ └──────────────┘ └────────────────┘ └────────────────┘
typ └───────────────────┘ └──────────────┘ └────────────────┘ └────────────────┘
573
574 lemma coe_Sup {s : set α} (hb : bdd_above s) : (↑(Sup s) : with_top α) = (⨆a∈s, ↑a) :=
id └─┘ ┴ └───────┘ ┴ ┴ └─┘ ┴ └──────┘ ┴ ┴ ┴┴ ┴┴ ┴┴
src └─┘ └───────┘ ┴ └─┘ └──────┘ ┴ ┴ ┴ ┴
typ └─┘ ┴ └───────┘ ┴ ┴ └─┘ ┴ └──────┘ ┴ ┴ ┴┴ ┴┴ ┴┴
doc └───────┘ └─┘ ┴ ┴
575 begin
st └─────
576 cases s.eq_empty_or_nonempty with hs hs,
id └────────────────────┘
src └────┘└────────────────────┘└─────────┘
typ └────┘└────────────────────┘└─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid ┴ └─────────┘
st ────────────────────────────────────────┘└─
577 { rw [hs, cSup_empty], simp only [set.mem_empty_eq, lattice.supr_bot, lattice.supr_false], refl },
id └┘ └────────┘ └──────────────┘ └──────────────┘ └────────────────┘
src └──┘ └┘└────────┘┴ └─────────┘└──────────────┘└┘└──────────────┘└┘└────────────────┘┴ └───┘
typ └──┘└┘└┘└────────┘┴ └─────────┘└──────────────┘└┘└──────────────┘└┘└────────────────┘┴ └───┘
doc └──┘ └┘ ┴ └─────────┘ └┘ └┘ ┴ └───┘
txt └──┘ └┘ ┴ └─────────┘ └┘ └┘ ┴ └───┘
par └──┘ └┘ ┴ └─────────┘ └┘ └┘ ┴ └───┘
pid └┘ └┘ ┴ ┴└──┘└┘ └┘ └┘ ┴ ┴
st ───┘└────┘└──────────┘┴└──────────────────────────────────────────────────────────────────┘└─────┘└┘└
578 apply le_antisymm,
id └─────────┘
src └────┘└─────────┘
typ └────┘└─────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────┘└─
579 { refine ((coe_le_iff _ _).2 $ assume b hb, cSup_le hs $ assume a has, coe_le_coe.1 $ hb ▸ _),
id └────────┘ └─────┘ └┘ └────────┘ ┴
src └─────┘ └────────┘└──────┘ ┴ └─────┘└─────┘┴ ┴ ┴ └──────┘└────────┘└─┘ ┴ ┴┴└─┘
typ └─────┘ └────────┘└──────┘ ┴ └─────┘└─────┘┴└┘┴ ┴ └──────┘└────────┘└─┘ ┴ ┴┴└─┘
doc └─────┘ └──────┘ ┴ └─────┘ ┴ ┴ ┴ └──────┘ └─┘ ┴ ┴ └─┘
txt └─────┘ └──────┘ ┴ └─────┘ ┴ ┴ ┴ └──────┘ └─┘ ┴ ┴ └─┘
par └─────┘ └──────┘ ┴ └─────┘ ┴ ┴ ┴ └──────┘ └─┘ ┴ ┴ └─┘
pid ┴ └──────┘ ┴ └─────┘ ┴ ┴ ┴ └──────┘ └─┘ ┴ ┴ └─┘
st ───┘└─────────────────────────────────────────────────────────────────────────────────────────┘└─
580 exact (le_supr_of_le a $ le_supr_of_le has $ _root_.le_refl _) },
id ┴ └───────────┘ └─┘ └────────────┘
src └────┘ ┴ ┴ ┴└───────────┘┴ ┴ ┴└────────────┘└──┘
typ └────┘ ┴┴┴ ┴└───────────┘┴└─┘┴ ┴└────────────┘└──┘
doc └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
txt └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
par └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘┴
st ──────────────────────────────────────────────────────────────────┘└┘└
581 { exact (supr_le $ assume a, supr_le $ assume ha, coe_le_coe.2 $ le_cSup hb ha) }
id └─────┘ └────────┘ └─────┘ └┘
src └────┘ ┴ ┴ └──┘└─────┘┴ ┴ └───┘└────────┘└─┘ ┴└─────┘┴ ┴ └┘
typ └────┘ ┴ ┴ └──┘└─────┘┴ ┴ └───┘└────────┘└─┘ ┴└─────┘┴└┘┴ └┘
doc └────┘ ┴ ┴ └──┘ ┴ ┴ └───┘ └─┘ ┴ ┴ ┴ └┘
txt └────┘ ┴ ┴ └──┘ ┴ ┴ └───┘ └─┘ ┴ ┴ ┴ └┘
par └────┘ ┴ ┴ └──┘ ┴ ┴ └───┘ └─┘ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ └──┘ ┴ ┴ └───┘ └─┘ ┴ ┴ ┴ ┴┴
st ─────────────────────────────────────────────────────────────────────────────────┘└─
582 end
st ──┘
583
584 lemma coe_Inf {s : set α} (hs : s.nonempty) : (↑(Inf s) : with_top α) = (⨅a∈s, ↑a) :=
id └─┘ ┴ ┴└───────┘ ┴ └─┘ ┴ └──────┘ ┴ ┴ ┴┴ ┴┴ ┴┴
src └─┘ └───────┘ ┴ └─┘ └──────┘ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴└───────┘ ┴ └─┘ ┴ └──────┘ ┴ ┴ ┴┴ ┴┴ ┴┴
doc └───────┘ └─┘ ┴ ┴
585 let ⟨x, hx⟩ := hs in
id └─┘ ┴ └┘ └┘
typ └─┘ ┴ └┘ └┘
586 have (⨅a∈s, ↑a : with_top α) ≤ x, from infi_le_of_le x $ infi_le_of_le hx $ _root_.le_refl _,
id ┴┴ ┴┴ ┴┴ └──────┘ ┴ ┴ └───────────┘ └───────────┘ └────────────┘
src ┴ ┴ ┴ └──────┘ ┴ └───────────┘ └───────────┘ └────────────┘
typ ┴┴ ┴┴ ┴┴ └──────┘ ┴ ┴ └───────────┘ └───────────┘ └────────────┘
doc ┴ ┴
587 let ⟨r, r_eq, hr⟩ := (le_coe_iff _ _).1 this in
id └─┘ └────────┘ ┴ └──┘
src └────────┘ ┴
typ └─┘ └────────┘ ┴ └──┘
588 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
589 (le_infi $ assume a, le_infi $ assume ha, coe_le_coe.2 $ cInf_le (bdd_below_bot s) ha)
id └─────┘ ┴ └─────┘ └┘ └────────┘┴ └─────┘ └───────────┘ ┴ └┘
src └─────┘ └─────┘ └────────┘┴ └─────┘ └───────────┘
typ └─────┘ ┴ └─────┘ └┘ └────────┘┴ └─────┘ └───────────┘ ┴ └┘
doc └───────────┘
590 begin
st └─────
591 refine (r_eq.symm ▸ coe_le_coe.2 $ le_cInf hs $ assume a has, coe_le_coe.1 $ _),
id └───────┘ ┴ └─────┘ └┘ └────────┘
src └─────┘ └───────┘┴┴┴ └─┘ ┴└─────┘┴ ┴ ┴ └──────┘└────────┘└─┘ └─┘
typ └─────┘ └───────┘┴┴┴ └─┘ ┴└─────┘┴└┘┴ ┴ └──────┘└────────┘└─┘ └─┘
doc └─────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └──────┘ └─┘ └─┘
txt └─────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └──────┘ └─┘ └─┘
par └─────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └──────┘ └─┘ └─┘
pid ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └──────┘ └─┘ └─┘
st ──────────────────────────────────────────────────────────────────────────────────┘└─
592 refine (r_eq ▸ infi_le_of_le a _),
id └──┘ └───────────┘ ┴
src └─────┘ ┴ ┴└───────────┘┴ └─┘
typ └─────┘ └──┘┴ ┴└───────────┘┴┴└─┘
doc └─────┘ ┴ ┴ ┴ └─┘
txt └─────┘ ┴ ┴ ┴ └─┘
par └─────┘ ┴ ┴ ┴ └─┘
pid ┴ ┴ ┴ ┴ └─┘
st ────────────────────────────────────┘└─
593 exact (infi_le_of_le has $ _root_.le_refl _),
id └───────────┘ └─┘ └────────────┘
src └────┘ └───────────┘┴ ┴ ┴└────────────┘└─┘
typ └────┘ └───────────┘┴└─┘┴ ┴└────────────┘└─┘
doc └────┘ ┴ ┴ ┴ └─┘
txt └────┘ ┴ ┴ ┴ └─┘
par └────┘ ┴ ┴ ┴ └─┘
pid ┴ ┴ ┴ ┴ └─┘
st ───────────────────────────────────────────────┘└─
594 end
st ────┘
595
596 end with_top
597
598 namespace enat
599 open_locale classical
600 open lattice
601
602 noncomputable instance : complete_linear_order enat :=
id └───────────────────┘ └──┘
src └───────────────────┘ └──┘
typ └───────────────────┘ └──┘
doc └───────────────────┘
603 { Sup := λ s, with_top_equiv.symm $ Sup (with_top_equiv '' s),
id ┴ └────────────┘└───┘ └─┘ └────────────┘ └┘ ┴
src └────────────┘└───┘ └─┘ └────────────┘ └┘
typ ┴ └────────────┘└───┘ └─┘ └────────────┘ └┘ ┴
doc └────────────┘ └─┘ └────────────┘
604 Inf := λ s, with_top_equiv.symm $ Inf (with_top_equiv '' s),
id ┴ └────────────┘└───┘ └─┘ └────────────┘ └┘ ┴
src └────────────┘└───┘ └─┘ └────────────┘ └┘
typ ┴ └────────────┘└───┘ └─┘ └────────────┘ └┘ ┴
doc └────────────┘ └─┘ └────────────┘
605 le_Sup := by intros; rw ← with_top_equiv_le; simp; apply le_Sup _; simpa,
id └───────────────┘ └────┘
src └────┘ └───┘└───────────────┘ └──┘ └────┘└────┘└┘ └───┘
typ └────┘ └───┘└───────────────┘ └──┘ └────┘└────┘└┘ └───┘
doc └────┘ └───┘ └──┘ └────┘ └┘ └───┘
txt └────┘ └───┘ └──┘ └────┘ └┘ └───┘
par └────┘ └───┘ └──┘ └────┘ └┘ └───┘
pid └─┘ ┴ └┘
st └──────────────────────────────────────────────────────────┘
606 Inf_le := by intros; rw ← with_top_equiv_le; simp; apply Inf_le _; simpa,
id └───────────────┘ └────┘
src └────┘ └───┘└───────────────┘ └──┘ └────┘└────┘└┘ └───┘
typ └────┘ └───┘└───────────────┘ └──┘ └────┘└────┘└┘ └───┘
doc └────┘ └───┘ └──┘ └────┘ └┘ └───┘
txt └────┘ └───┘ └──┘ └────┘ └┘ └───┘
par └────┘ └───┘ └──┘ └────┘ └┘ └───┘
pid └─┘ ┴ └┘
st └──────────────────────────────────────────────────────────┘
607 Sup_le := begin
st └─────
608 intros s a h1,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └─────┘
st ────────────────┘└─
609 rw [← with_top_equiv_le, with_top_equiv.right_inverse_symm],
id └───────────────┘
src └────┘└───────────────┘└┘ ┴
typ └────┘└───────────────┘└┘└───────────────────────────────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid └──┘ └┘ ┴
st ──────────────────────────┘└─────────────────────────────────┘└──
610 apply Sup_le _,
id └────┘
src └────┘└────┘└┘
typ └────┘└────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ └┘
st ─────────────────┘└─
611 rintros b ⟨x, h2, rfl⟩,
src └────────────────────┘
typ └────────────────────┘
doc └────────────────────┘
txt └────────────────────┘
par └────────────────────┘
pid └─────────────┘
st ─────────────────────────┘└─
612 rw with_top_equiv_le,
id └───────────────┘
src └─┘└───────────────┘
typ └─┘└───────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────────────┘└─
613 apply h1,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────┘└─
614 assumption
src └──────────
typ └──────────
doc └──────────
txt └──────────
par └──────────
pid └
st ───────────────
615 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
616 le_Inf := begin
st └─────
617 intros s a h1,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └─────┘
st ────────────────┘└─
618 rw [← with_top_equiv_le, with_top_equiv.right_inverse_symm],
id └───────────────┘
src └────┘└───────────────┘└┘ ┴
typ └────┘└───────────────┘└┘└───────────────────────────────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid └──┘ └┘ ┴
st ──────────────────────────┘└─────────────────────────────────┘└──
619 apply le_Inf _,
id └────┘
src └────┘└────┘└┘
typ └────┘└────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ └┘
st ─────────────────┘└─
620 rintros b ⟨x, h2, rfl⟩,
src └────────────────────┘
typ └────────────────────┘
doc └────────────────────┘
txt └────────────────────┘
par └────────────────────┘
pid └─────────────┘
st ─────────────────────────┘└─
621 rw with_top_equiv_le,
id └───────────────┘
src └─┘└───────────────┘
typ └─┘└───────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────────────┘└─
622 apply h1,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────┘└─
623 assumption
src └──────────
typ └──────────
doc └──────────
txt └──────────
par └──────────
pid └
st ───────────────
624 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
625 ..enat.decidable_linear_order,
id └─────────────────────────┘
src └─────────────────────────┘
typ └─────────────────────────┘
626 ..enat.lattice.bounded_lattice }
id └──────────────────────────┘
src └──────────────────────────┘
typ └──────────────────────────┘
627
628 end enat
629
630 section order_dual
631 open lattice
632
633 instance (α : Type*) [conditionally_complete_lattice α] :
id └────────────────────────────┘ ┴
src └────────────────────────────┘
typ └────────────────────────────┘ ┴
doc └────────────────────────────┘
634 conditionally_complete_lattice (order_dual α) :=
id └────────────────────────────┘ └────────┘ ┴
src └────────────────────────────┘ └────────┘
typ └────────────────────────────┘ └────────┘ ┴
doc └────────────────────────────┘ └────────┘
635 { le_cSup := @cInf_le α _,
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
636 cSup_le := @le_cInf α _,
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
637 le_cInf := @cSup_le α _,
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
638 cInf_le := @le_cSup α _,
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
639 ..order_dual.lattice.has_Inf α,
id └────────────────────────┘ ┴
src └────────────────────────┘
typ └────────────────────────┘ ┴
640 ..order_dual.lattice.has_Sup α,
id └────────────────────────┘ ┴
src └────────────────────────┘
typ └────────────────────────┘ ┴
641 ..order_dual.lattice.lattice α }
id └────────────────────────┘ ┴
src └────────────────────────┘
typ └────────────────────────┘ ┴
642
643 instance (α : Type*) [conditionally_complete_linear_order α] :
id └─────────────────────────────────┘ ┴
src └─────────────────────────────────┘
typ └─────────────────────────────────┘ ┴
644 conditionally_complete_linear_order (order_dual α) :=
id └─────────────────────────────────┘ └────────┘ ┴
src └─────────────────────────────────┘ └────────┘
typ └─────────────────────────────────┘ └────────┘ ┴
doc └────────┘
645 { ..order_dual.lattice.conditionally_complete_lattice α,
id └───────────────────────────────────────────────┘ ┴
src └───────────────────────────────────────────────┘
typ └───────────────────────────────────────────────┘ ┴
646 ..order_dual.decidable_linear_order α }
id └───────────────────────────────┘ ┴
src └───────────────────────────────┘
typ └───────────────────────────────┘ ┴
647
648 end order_dual
649
650 section with_top_bot
651
652 /-! ### Complete lattice structure on `with_top (with_bot α)`
653
654 If `α` is a `conditionally_complete_lattice`, then we show that `with_top α` and `with_bot α`
655 also inherit the structure of conditionally complete lattices. Furthermore, we show
656 that `with_top (with_bot α)` naturally inherits the structure of a complete lattice. Note that
657 for α a conditionally complete lattice, `Sup` and `Inf` both return junk values
658 for sets which are empty or unbounded. The extension of `Sup` to `with_top α` fixes
659 the unboundedness problem and the extension to `with_bot α` fixes the problem with
660 the empty set.
661
662 This result can be used to show that the extended reals [-∞, ∞] are a complete lattice.
663 -/
664
665 open lattice
666
667 open_locale classical
668
669 /-- Adding a top element to a conditionally complete lattice gives a conditionally complete lattice -/
670 noncomputable instance with_top.conditionally_complete_lattice
671 {α : Type*} [conditionally_complete_lattice α] :
id └────────────────────────────┘ ┴
src └────────────────────────────┘
typ └────────────────────────────┘ ┴
doc └────────────────────────────┘
672 conditionally_complete_lattice (with_top α) :=
id └────────────────────────────┘ └──────┘ ┴
src └────────────────────────────┘ └──────┘
typ └────────────────────────────┘ └──────┘ ┴
doc └────────────────────────────┘
673 { le_cSup := λ S a hS haS, (with_top.is_lub_Sup' ⟨a, haS⟩).1 haS,
id ┴ ┴ └┘ └─┘ └──────────────────┘ ┴ └─┘ ┴ └─┘
src └──────────────────┘ ┴
typ ┴ ┴ └┘ └─┘ └──────────────────┘ ┴ └─┘ ┴ └─┘
doc └──────────────────┘
674 cSup_le := λ S a hS haS, (with_top.is_lub_Sup' hS).2 haS,
id ┴ ┴ └┘ └─┘ └──────────────────┘ └┘ ┴ └─┘
src └──────────────────┘ ┴
typ ┴ ┴ └┘ └─┘ └──────────────────┘ └┘ ┴ └─┘
doc └──────────────────┘
675 cInf_le := λ S a hS haS, (with_top.is_glb_Inf' hS).1 haS,
id ┴ ┴ └┘ └─┘ └──────────────────┘ └┘ ┴ └─┘
src └──────────────────┘ ┴
typ ┴ ┴ └┘ └─┘ └──────────────────┘ └┘ ┴ └─┘
doc └──────────────────┘
676 le_cInf := λ S a hS haS, (with_top.is_glb_Inf' ⟨a, haS⟩).2 haS,
id ┴ ┴ └┘ └─┘ └──────────────────┘ ┴ └─┘ ┴ └─┘
src └──────────────────┘ ┴
typ ┴ ┴ └┘ └─┘ └──────────────────┘ ┴ └─┘ ┴ └─┘
doc └──────────────────┘
677 ..with_top.lattice,
id └──────────────┘
src └──────────────┘
typ └──────────────┘
678 ..with_top.lattice.has_Sup,
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
679 ..with_top.lattice.has_Inf }
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
680
681 /-- Adding a bottom element to a conditionally complete lattice gives a conditionally complete lattice -/
682 noncomputable instance with_bot.conditionally_complete_lattice
683 {α : Type*} [conditionally_complete_lattice α] :
id └────────────────────────────┘ ┴
src └────────────────────────────┘
typ └────────────────────────────┘ ┴
doc └────────────────────────────┘
684 conditionally_complete_lattice (with_bot α) :=
id └────────────────────────────┘ └──────┘ ┴
src └────────────────────────────┘ └──────┘
typ └────────────────────────────┘ └──────┘ ┴
doc └────────────────────────────┘
685 { le_cSup := (@with_top.conditionally_complete_lattice (order_dual α) _).cInf_le,
id └─────────────────────────────────────┘ └────────┘ ┴ └─────┘
src └─────────────────────────────────────┘ └────────┘ └─────┘
typ └─────────────────────────────────────┘ └────────┘ ┴ └─────┘
doc └─────────────────────────────────────┘ └────────┘
686 cSup_le := (@with_top.conditionally_complete_lattice (order_dual α) _).le_cInf,
id └─────────────────────────────────────┘ └────────┘ ┴ └─────┘
src └─────────────────────────────────────┘ └────────┘ └─────┘
typ └─────────────────────────────────────┘ └────────┘ ┴ └─────┘
doc └─────────────────────────────────────┘ └────────┘
687 cInf_le := (@with_top.conditionally_complete_lattice (order_dual α) _).le_cSup,
id └─────────────────────────────────────┘ └────────┘ ┴ └─────┘
src └─────────────────────────────────────┘ └────────┘ └─────┘
typ └─────────────────────────────────────┘ └────────┘ ┴ └─────┘
doc └─────────────────────────────────────┘ └────────┘
688 le_cInf := (@with_top.conditionally_complete_lattice (order_dual α) _).cSup_le,
id └─────────────────────────────────────┘ └────────┘ ┴ └─────┘
src └─────────────────────────────────────┘ └────────┘ └─────┘
typ └─────────────────────────────────────┘ └────────┘ ┴ └─────┘
doc └─────────────────────────────────────┘ └────────┘
689 ..with_bot.lattice,
id └──────────────┘
src └──────────────┘
typ └──────────────┘
690 ..with_bot.lattice.has_Sup,
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
691 ..with_bot.lattice.has_Inf }
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
692
693 /-- Adding a bottom and a top to a conditionally complete lattice gives a bounded lattice-/
694 noncomputable instance {α : Type*} [conditionally_complete_lattice α] : bounded_lattice (with_top (with_bot α)) :=
id └────────────────────────────┘ ┴ └─────────────┘ └──────┘ └──────┘ ┴
src └────────────────────────────┘ └─────────────┘ └──────┘ └──────┘
typ └────────────────────────────┘ ┴ └─────────────┘ └──────┘ └──────┘ ┴
doc └────────────────────────────┘ └─────────────┘
695 { ..with_top.order_bot,
id └────────────────┘
src └────────────────┘
typ └────────────────┘
696 ..with_top.order_top,
id └────────────────┘
src └────────────────┘
typ └────────────────┘
697 ..conditionally_complete_lattice.to_lattice _ }
id └───────────────────────────────────────┘
src └───────────────────────────────────────┘
typ └───────────────────────────────────────┘
698
699 theorem with_bot.cSup_empty {α : Type*} [conditionally_complete_lattice α] :
id └────────────────────────────┘ ┴
src └────────────────────────────┘
typ └────────────────────────────┘ ┴
doc └────────────────────────────┘
700 Sup (∅ : set (with_bot α)) = ⊥ :=
id └─┘ ┴ └─┘ └──────┘ ┴ ┴ ┴
src └─┘ ┴ └─┘ └──────┘ ┴ ┴
typ └─┘ ┴ └─┘ └──────┘ ┴ ┴ ┴
doc └─┘
701 begin
st └─────
702 show ite _ _ _ = ⊥,
id └─┘ ┴ ┴
src └───┘└─┘└─────┘┴┴┴
typ └───┘└─┘└─────┘┴┴┴
doc └───┘ └─────┘ ┴
txt └───┘ └─────┘ ┴
par └───┘ └─────┘ ┴
pid └───┘ └─────┘ ┴
st ───────────────────┘└─
703 split_ifs; finish,
src └───────┘ └────┘
typ └───────┘ └────┘
doc └───────┘ └────┘
txt └───────┘ └────┘
par └───────┘ └────┘
st ──────────────────┘└─
704 end
st ──┘
705
706 noncomputable instance {α : Type*} [conditionally_complete_lattice α] :
id └────────────────────────────┘ ┴
src └────────────────────────────┘
typ └────────────────────────────┘ ┴
doc └────────────────────────────┘
707 complete_lattice (with_top (with_bot α)) :=
id └──────────────┘ └──────┘ └──────┘ ┴
src └──────────────┘ └──────┘ └──────┘
typ └──────────────┘ └──────┘ └──────┘ ┴
doc └──────────────┘
708 { le_Sup := λ S a haS, (with_top.is_lub_Sup' ⟨a, haS⟩).1 haS,
id ┴ ┴ └─┘ └──────────────────┘ ┴ └─┘ ┴ └─┘
src └──────────────────┘ ┴
typ ┴ ┴ └─┘ └──────────────────┘ ┴ └─┘ ┴ └─┘
doc └──────────────────┘
709 Sup_le := λ S a ha,
id ┴ ┴ └┘
typ ┴ ┴ └┘
710 begin
st └─────
711 cases S.eq_empty_or_nonempty with h,
id └────────────────────┘
src └────┘└────────────────────┘└─────┘
typ └────┘└────────────────────┘└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ └─────┘
st ────────────────────────────────────────┘└─
712 { show ite _ _ _ ≤ a,
id └─┘ ┴ ┴
src └───┘└─┘└─────┘┴┴
typ └───┘└─┘└─────┘┴┴┴
doc └───┘ └─────┘ ┴
txt └───┘ └─────┘ ┴
par └───┘ └─────┘ ┴
pid └───┘ └─────┘ ┴
st ───────┘└────────────────┘└─
713 split_ifs,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
st ────────────────┘└─
714 { rw h at h_1, cases h_1 },
id ┴ └─┘
src └─┘ └─────┘ └────┘ ┴
typ └─┘┴└─────┘ └────┘└─┘┴
doc └─┘ └─────┘ └────┘ ┴
txt └─┘ └─────┘ └────┘ ┴
par └─┘ └─────┘ └────┘ ┴
pid ┴ └─────┘ ┴ ┴
st ─────────┘└─────────┘└──────────┘└┘└
715 { convert bot_le, convert with_bot.cSup_empty, rw h, refl },
id └────┘ └─────────────────┘ ┴
src └──────┘└────┘ └──────┘└─────────────────┘ └─┘ └───┘
typ └──────┘└────┘ └──────┘└─────────────────┘ └─┘┴ └───┘
doc └──────┘ └──────┘ └─┘ └───┘
txt └──────┘ └──────┘ └─┘ └───┘
par └──────┘ └──────┘ └─┘ └───┘
pid ┴ ┴ ┴ ┴
st ─────────┘└────────────┘└───────────────────────────┘└────┘└─────┘└┘└
716 { exfalso, apply h_2, use ⊥, rw h, rintro b ⟨⟩ } },
id ┴ ┴
src └─────┘ └────┘ └──┘┴ └─┘ └──────────┘
typ └─────┘ └────┘ └──┘┴ └─┘┴ └──────────┘
doc └─────┘ └────┘ └──┘ └─┘ └──────────┘
txt └─────┘ └────┘ └──┘ └─┘ └──────────┘
par └─────┘ └────┘ └──┘ └─┘ └──────────┘
pid ┴ ┴ ┴ └───┘┴
st ────────────────┘└─────────┘└─────┘└────┘└────────────┘└──┘└
717 { refine (with_top.is_lub_Sup' h).2 ha }
id └──────────────────┘ ┴ └┘
src └─────┘ └──────────────────┘┴ └──┘ ┴
typ └─────┘ └──────────────────┘┴┴└──┘└┘┴
doc └─────┘ └──────────────────┘┴ └──┘ ┴
txt └─────┘ ┴ └──┘ ┴
par └─────┘ ┴ └──┘ ┴
pid ┴ ┴ └──┘ ┴
st ────────────────────────────────────────────┘└─
718 end,
st ──────┘
719 Inf_le := λ S a haS,
id ┴ ┴ └─┘
typ ┴ ┴ └─┘
720 show ite _ _ _ ≤ a,
id └─┘ ┴ ┴
src └─┘ ┴
typ └─┘ ┴ ┴
721 begin
st └─────
722 split_ifs,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
st ──────────────┘└─
723 { cases a with a, exact _root_.le_refl _,
id ┴ └────────────┘
src └────┘ └─────┘ └────┘└────────────┘└┘
typ └────┘┴└─────┘ └────┘└────────────┘└┘
doc └────┘ └─────┘ └────┘ └┘
txt └────┘ └─────┘ └────┘ └┘
par └────┘ └─────┘ └────┘ └┘
pid ┴ └─────┘ ┴ └┘
st ───────┘└────────────┘└──────────────────────┘└─
724 cases (h haS); tauto },
id ┴ └─┘
src └────┘ ┴ ┴ └────┘
typ └────┘ ┴┴└─┘┴ └────┘
doc └────┘ ┴ ┴ └────┘
txt └────┘ ┴ ┴ └────┘
par └────┘ ┴ ┴ └────┘
pid ┴ ┴ ┴ ┴
st ────────────────────────────┘└┘└
725 { cases a,
id ┴
src └────┘
typ └────┘┴
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────┘└─
726 { exact le_top },
id └────┘
src └────┘└────┘┴
typ └────┘└────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────┘└───────────┘└┘└
727 { apply with_top.some_le_some.2, refine cInf_le _ haS, use ⊥, intros b hb, exact bot_le } }
id └───────────────────┘ └─────┘ └─┘ └────┘
src └────┘└───────────────────┘└┘ └─────┘└─────┘└─┘ └──┘ └─────────┘ └────┘└────┘┴
typ └────┘└───────────────────┘└┘ └─────┘└─────┘└─┘└─┘ └──┘ └─────────┘ └────┘└────┘┴
doc └────┘ └┘ └─────┘ └─┘ └──┘ └─────────┘ └────┘ ┴
txt └────┘ └┘ └─────┘ └─┘ └──┘ └─────────┘ └────┘ ┴
par └────┘ └┘ └─────┘ └─┘ └──┘ └─────────┘ └────┘ ┴
pid ┴ └┘ ┴ └─┘ ┴ └───┘ ┴ ┴
st ──────────────────────────────────────┘└────────────────────┘└─────┘└───────────┘└─────────────┘└───
728 end,
st ──────┘
729 le_Inf := λ S a haS, (with_top.is_glb_Inf' ⟨a, haS⟩).2 haS,
id ┴ ┴ └─┘ └──────────────────┘ ┴ └─┘ ┴ └─┘
src └──────────────────┘ ┴
typ ┴ ┴ └─┘ └──────────────────┘ ┴ └─┘ ┴ └─┘
doc └──────────────────┘
730 ..with_top.lattice.has_Inf,
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
731 ..with_top.lattice.has_Sup,
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
732 ..with_top.lattice.bounded_lattice }
id └──────────────────────────────┘
src └──────────────────────────────┘
typ └──────────────────────────────┘
doc └──────────────────────────────┘
733
734 end with_top_bot